diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-17 18:33:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-17 18:33:16 +0000 |
| commit | 9b24b6d763bb2c7975cd2b93364d7647fd660598 (patch) | |
| tree | bc4733a59179e67274c9c82ac18db28b2e9d4a23 /test-suite/output/Search.out | |
| parent | 248e7beca97c073d0f5a2f937d77f2c4d8c805df (diff) | |
Renaming SearchAbout into Search and Search into SearchHead.
I hope I did not forget any place to change.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16423 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Search.out')
| -rw-r--r-- | test-suite/output/Search.out | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index 2a22a89b6..120c6a4ea 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,29 +1,29 @@ -le_S: forall n m : nat, n <= m -> n <= S m le_n: forall n : nat, n <= n +le_S: forall n m : nat, n <= m -> n <= S m le_pred: forall n m : nat, n <= m -> pred n <= pred m le_S_n: forall n m : nat, S n <= S m -> n <= m -false: bool true: bool -xorb: bool -> bool -> bool +false: bool +andb: bool -> bool -> bool orb: bool -> bool -> bool -negb: bool -> bool implb: bool -> bool -> bool -andb: bool -> bool -> bool -pred_Sn: forall n : nat, n = pred (S n) -plus_n_Sm: forall n m : nat, S (n + m) = n + S m -plus_n_O: forall n : nat, n = n + 0 -plus_Sn_m: forall n m : nat, S n + m = S (n + m) -plus_O_n: forall n : nat, 0 + n = n -mult_n_Sm: forall n m : nat, n * m + n = n * S m -mult_n_O: forall n : nat, 0 = n * 0 -min_r: forall n m : nat, m <= n -> min n m = m -min_l: forall n m : nat, n <= m -> min n m = n -max_r: forall n m : nat, n <= m -> max n m = m -max_l: forall n m : nat, m <= n -> max n m = n +xorb: bool -> bool -> bool +negb: bool -> bool +eq_S: forall x y : nat, x = y -> S x = S y f_equal_pred: forall x y : nat, x = y -> pred x = pred y +pred_Sn: forall n : nat, n = pred (S n) +eq_add_S: forall n m : nat, S n = S m -> n = m f_equal2_plus: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2 +plus_n_O: forall n : nat, n = n + 0 +plus_O_n: forall n : nat, 0 + n = n +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +plus_Sn_m: forall n m : nat, S n + m = S (n + m) f_equal2_mult: forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2 -eq_add_S: forall n m : nat, S n = S m -> n = m -eq_S: forall x y : nat, x = y -> S x = S y +mult_n_O: forall n : nat, 0 = n * 0 +mult_n_Sm: forall n m : nat, n * m + n = n * S m +max_l: forall n m : nat, m <= n -> max n m = n +max_r: forall n m : nat, n <= m -> max n m = m +min_l: forall n m : nat, n <= m -> min n m = n +min_r: forall n m : nat, m <= n -> min n m = m |