diff options
Diffstat (limited to 'test-suite/output/SearchHead.out')
| -rw-r--r-- | test-suite/output/SearchHead.out | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 61ceab72f8..9554581ebe 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -1,9 +1,17 @@ +File "stdin", line 3, characters 0-14: +Warning: +SearchHead is deprecated. Use the headconcl: clause of Search instead. +[deprecated-searchhead,deprecated] le_n: forall n : nat, n <= n le_0_n: forall n : nat, 0 <= n le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m le_n_S: forall n m : nat, n <= m -> S n <= S m le_S_n: forall n m : nat, S n <= S m -> n <= m +File "stdin", line 4, characters 0-16: +Warning: +SearchHead is deprecated. Use the headconcl: clause of Search instead. +[deprecated-searchhead,deprecated] false: bool true: bool negb: bool -> bool @@ -27,6 +35,10 @@ Hexadecimal.uint_beq: Hexadecimal.uint -> Hexadecimal.uint -> bool Decimal.decimal_beq: Decimal.decimal -> Decimal.decimal -> bool Decimal.int_beq: Decimal.int -> Decimal.int -> bool Decimal.uint_beq: Decimal.uint -> Decimal.uint -> bool +File "stdin", line 5, characters 0-21: +Warning: +SearchHead is deprecated. Use the headconcl: clause of Search instead. +[deprecated-searchhead,deprecated] mult_n_O: forall n : nat, 0 = n * 0 plus_O_n: forall n : nat, 0 + n = n plus_n_O: forall n : nat, n = n + 0 @@ -45,5 +57,13 @@ f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 +File "stdin", line 11, characters 2-20: +Warning: +SearchHead is deprecated. Use the headconcl: clause of Search instead. +[deprecated-searchhead,deprecated] h: newdef n +File "stdin", line 17, characters 2-15: +Warning: +SearchHead is deprecated. Use the headconcl: clause of Search instead. +[deprecated-searchhead,deprecated] h: P n |