diff options
Diffstat (limited to 'test-suite/output')
| -rw-r--r-- | test-suite/output/Arguments.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 14 | ||||
| -rw-r--r-- | test-suite/output/Errors.out | 2 | ||||
| -rw-r--r-- | test-suite/output/FunExt.out | 19 | ||||
| -rw-r--r-- | test-suite/output/FunExt.v | 168 | ||||
| -rw-r--r-- | test-suite/output/Notations.out | 20 | ||||
| -rw-r--r-- | test-suite/output/Search.out | 114 | ||||
| -rw-r--r-- | test-suite/output/SearchHead.out | 42 | ||||
| -rw-r--r-- | test-suite/output/SearchPattern.out | 84 | ||||
| -rw-r--r-- | test-suite/output/ShowProof.out | 1 | ||||
| -rw-r--r-- | test-suite/output/ShowProof.v | 6 | ||||
| -rw-r--r-- | test-suite/output/auto.out | 20 | ||||
| -rw-r--r-- | test-suite/output/auto.v | 11 | ||||
| -rw-r--r-- | test-suite/output/ltac.out | 5 | ||||
| -rw-r--r-- | test-suite/output/ltac_missing_args.out | 20 | ||||
| -rw-r--r-- | test-suite/output/ltac_missing_args.v | 19 |
16 files changed, 406 insertions, 143 deletions
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out index a2ee2d4c8e..979396969a 100644 --- a/test-suite/output/Arguments.out +++ b/test-suite/output/Arguments.out @@ -97,8 +97,8 @@ Expands to: Constant Top.f forall w : r, w 3 true = tt : Prop The command has indeed failed with message: -Error: Unknown interpretation for notation "$". +Unknown interpretation for notation "$". w 3 true = tt : Prop The command has indeed failed with message: -Error: Extra arguments: _, _. +Extra arguments: _, _. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index b084ad4984..4df21ae353 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -1,5 +1,5 @@ The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +To rename arguments the "rename" flag must be specified. Argument A renamed to B. File "stdin", line 2, characters 0-25: Warning: This command is just asserting the names of arguments of identity. @@ -103,15 +103,15 @@ Expands to: Constant Top.myplus @myplus : forall Z : Type, Z -> nat -> nat -> nat The command has indeed failed with message: -Error: Argument lists should agree on the names they provide. +Argument lists should agree on the names they provide. The command has indeed failed with message: -Error: Sequences of implicit arguments must be of different lengths. +Sequences of implicit arguments must be of different lengths. The command has indeed failed with message: -Error: Some argument names are duplicated: F +Some argument names are duplicated: F The command has indeed failed with message: -Error: Argument z cannot be declared implicit. +Argument z cannot be declared implicit. The command has indeed failed with message: -Error: Extra arguments: y. +Extra arguments: y. The command has indeed failed with message: -Error: To rename arguments the "rename" flag must be specified. +To rename arguments the "rename" flag must be specified. Argument A renamed to R. diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 06a6b2d157..38d055b28e 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -7,4 +7,4 @@ In nested Ltac calls to "f" and "apply x", last call failed. Unable to unify "nat" with "True". The command has indeed failed with message: Ltac call to "instantiate ( (ident) := (lglob) )" failed. -Error: Instance is not well-typed in the environment of ?x. +Instance is not well-typed in the environment of ?x. diff --git a/test-suite/output/FunExt.out b/test-suite/output/FunExt.out new file mode 100644 index 0000000000..8d2a125c1d --- /dev/null +++ b/test-suite/output/FunExt.out @@ -0,0 +1,19 @@ +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Not an extensional equality. +The command has indeed failed with message: +Ltac call to "extensionality in (var)" failed. +Tactic failure: Already an intensional equality. +The command has indeed failed with message: +In nested Ltac calls to "extensionality in (var)" and +"clearbody (ne_var_list)", last call failed. +Hypothesis e depends on the body of H' diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v new file mode 100644 index 0000000000..7658ce718e --- /dev/null +++ b/test-suite/output/FunExt.v @@ -0,0 +1,168 @@ +Require Import FunctionalExtensionality. + +(* Basic example *) +Goal (forall x y z, x+y+z = z+y+x) -> (fun x y z => z+y+x) = (fun x y z => x+y+z). +intro H. +extensionality in H. +symmetry in H. +assumption. +Qed. + +(* Test rejection of non-equality *) +Goal forall H:(forall A:Prop, A), H=H -> forall H'':True, H''=H''. +intros H H' H''. +Fail extensionality in H. +clear H'. +Fail extensionality in H. +Fail extensionality in H''. +Abort. + +(* Test success on dependent equality *) +Goal forall (p : forall x, S x = x + 1), p = p -> S = fun x => x + 1. +intros p H. +extensionality in p. +assumption. +Qed. + +(* Test dependent functional extensionality *) +Goal forall (P:nat->Type) (Q:forall a, P a -> Type) (f g:forall a (b:P a), Q a b), + (forall x y, f x y = g x y) -> f = g. +intros * H. +extensionality in H. +assumption. +Qed. + +(* Other tests, courtesy of Jason Gross *) + +Goal forall A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c), (forall a b c, f a b c = g a b c) -> f = g. +Proof. + intros A B C D f g H. + extensionality in H. + match type of H with f = g => idtac end. + exact H. +Qed. + +Section test_section. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, f a b c = g a b c). + Goal f = g. + Proof. + extensionality in H. + match type of H with f = g => idtac end. + exact H. + Qed. +End test_section. + +Section test2. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall b a c, f a b c = g a b c). + Goal (fun b a c => f a b c) = (fun b a c => g a b c). + Proof. + extensionality in H. + match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end. + exact H. + Qed. +End test2. + +Section test3. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a c, (fun b => f a b c) = (fun b => g a b c)). + Goal (fun a c b => f a b c) = (fun a c b => g a b c). + Proof. + extensionality in H. + match type of H with (fun a c b => f a b c) = (fun a' c' b' => g a' b' c') => idtac end. + exact H. + Qed. +End test3. + +Section test4. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c -> Type) + (H : forall b, (forall a c d, f a b c d) = (forall a c d, g a b c d)). + Goal (fun b => forall a c d, f a b c d) = (fun b => forall a c d, g a b c d). + Proof. + extensionality in H. + exact H. + Qed. +End test4. + +Section test5. + Goal nat -> True. + Proof. + intro n. + Fail extensionality in n. + constructor. + Qed. +End test5. + +Section test6. + Goal let f := fun A (x : A) => x in let pf := fun A x => @eq_refl _ (f A x) in f = f. + Proof. + intros f pf. + extensionality in pf. + match type of pf with f = f => idtac end. + exact pf. + Qed. +End test6. + +Section test7. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, True -> f a b c = g a b c). + Goal True. + Proof. + extensionality in H. + match type of H with (fun a b c (_ : True) => f a b c) = (fun a' b' c' (_ : True) => g a' b' c') => idtac end. + constructor. + Qed. +End test7. + +Section test8. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : True -> forall a b c, f a b c = g a b c). + Goal True. + Proof. + extensionality in H. + match type of H with (fun (_ : True) => f) = (fun (_ : True) => g) => idtac end. + constructor. + Qed. +End test8. + +Section test9. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall b a c, f a b c = g a b c). + Goal (fun b a c => f a b c) = (fun b a c => g a b c). + Proof. + pose H as H'. + extensionality in H. + extensionality in H'. + let T := type of H in let T' := type of H' in constr_eq T T'. + match type of H with (fun b a => f a b) = (fun b' a' => g a' b') => idtac end. + exact H'. + Qed. +End test9. + +Section test10. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : f = g). + Goal True. + Proof. + Fail extensionality in H. + constructor. + Qed. +End test10. + +Section test11. + Context A B C (D : forall a : A, C a -> Type) (f g : forall a : A, B -> forall c : C a, D a c) + (H : forall a b c, f a b c = f a b c). + Goal True. + Proof. + pose H as H'. + pose (eq_refl : H = H') as e. + extensionality in H. + Fail extensionality in H'. + clear e. + extensionality in H'. + let T := type of H in let T' := type of H' in constr_eq T T'. + lazymatch type of H with f = f => idtac end. + constructor. + Qed. +End test11. diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out index 26eaca8272..9d106d2dac 100644 --- a/test-suite/output/Notations.out +++ b/test-suite/output/Notations.out @@ -41,29 +41,29 @@ fun x : nat => ifn x is succ n then n else 0 -4 : Z The command has indeed failed with message: -Error: x should not be bound in a recursive pattern of the right-hand side. +x should not be bound in a recursive pattern of the right-hand side. The command has indeed failed with message: -Error: in the right-hand side, y and z should appear in +in the right-hand side, y and z should appear in term position as part of a recursive pattern. The command has indeed failed with message: The reference w was not found in the current environment. The command has indeed failed with message: -Error: in the right-hand side, y and z should appear in +in the right-hand side, y and z should appear in term position as part of a recursive pattern. The command has indeed failed with message: -Error: z is expected to occur in binding position in the right-hand side. +z is expected to occur in binding position in the right-hand side. The command has indeed failed with message: -Error: as y is a non-closed binder, no such "," is allowed to occur. +as y is a non-closed binder, no such "," is allowed to occur. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Cannot find where the recursive pattern starts. +Cannot find where the recursive pattern starts. The command has indeed failed with message: -Error: Both ends of the recursive pattern are the same. +Both ends of the recursive pattern are the same. SUM (nat * nat) nat : Set FST (0; 1) diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out index c17b285bc9..81fda176ec 100644 --- a/test-suite/output/Search.out +++ b/test-suite/output/Search.out @@ -1,108 +1,108 @@ 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_n_S: forall n m : nat, n <= m -> S n <= S m +le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m +le_S_n: forall n m : nat, S n <= S m -> n <= m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +min_r: forall n m : nat, m <= n -> Nat.min n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n le_ind: forall (n : nat) (P : nat -> Prop), P n -> (forall m : nat, n <= m -> P m -> P (S m)) -> forall n0 : nat, n <= n0 -> P n0 -le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m -le_S_n: forall n m : nat, S n <= S m -> n <= m -le_0_n: forall n : nat, 0 <= n -le_n_S: forall n m : nat, n <= m -> S n <= S m -max_l: forall n m : nat, m <= n -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m -true: bool false: bool -bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b -bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b -bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b -andb: bool -> bool -> bool -orb: bool -> bool -> bool -implb: bool -> bool -> bool -xorb: bool -> bool -> bool +true: bool +is_true: bool -> Prop negb: bool -> bool -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true -andb_true_intro: - forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true eq_true: bool -> Prop -eq_true_rect: - forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b -eq_true_ind: - forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b +implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool +xorb: bool -> bool -> bool +Nat.even: nat -> bool +Nat.odd: nat -> bool +BoolSpec: Prop -> Prop -> bool -> Prop +Nat.eqb: nat -> nat -> bool +Nat.testbit: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool +Nat.leb: nat -> nat -> bool +Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat +bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b +bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b eq_true_rec: forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b -is_true: bool -> Prop -eq_true_ind_r: - forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true -eq_true_rec_r: - forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_ind: + forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b eq_true_rect_r: forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true -BoolSpec: Prop -> Prop -> bool -> Prop +eq_true_rec_r: + forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true +eq_true_rect: + forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b +bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b +eq_true_ind_r: + forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true +andb_true_intro: + forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true BoolSpec_ind: forall (P Q : Prop) (P0 : bool -> Prop), (P -> P0 true) -> (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool -Nat.even: nat -> bool -Nat.odd: nat -> bool -Nat.testbit: nat -> nat -> bool -Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat bool_choice: forall (S : Set) (R1 R2 : S -> Prop), (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} -eq_S: forall x y : nat, x = y -> S x = S y -f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y -f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +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 +n_Sn: forall n : nat, n <> S n pred_Sn: forall n : nat, n = Nat.pred (S n) +O_S: forall n : nat, 0 <> S n +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +eq_S: forall x y : nat, x = y -> S x = S y eq_add_S: forall n m : nat, S n = S m -> n = m +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = n +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +plus_Sn_m: forall n m : nat, S n + m = S (n + m) +plus_n_Sm: forall n m : nat, S (n + m) = n + S m +f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y not_eq_S: forall n m : nat, n <> m -> S n <> S m -O_S: forall n : nat, 0 <> S n -n_Sn: forall n : nat, n <> S n +mult_n_Sm: forall n m : nat, n * m + n = n * S m 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 f_equal2_nat: forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat), x1 = y1 -> x2 = y2 -> f x1 x2 = f 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 -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 -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true bool_choice: forall (S : Set) (R1 R2 : S -> Prop), (forall x : S, {R1 x} + {R2 x}) -> {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x} -andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true andb_true_intro: forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true -h': newdef n <> n +andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true h: n <> newdef n h': newdef n <> n h: n <> newdef n +h': newdef n <> n h: n <> newdef n h: n <> newdef n -h': ~ P n h: P n h': ~ P n h: P n h': ~ P n h: P n +h': ~ P n h: P n h: P n diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out index 0d5924ec61..7038eac22c 100644 --- a/test-suite/output/SearchHead.out +++ b/test-suite/output/SearchHead.out @@ -1,39 +1,39 @@ 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_S_n: forall n m : nat, S n <= S m -> n <= m -le_0_n: forall n : nat, 0 <= n le_n_S: forall n m : nat, n <= m -> S n <= S m -true: bool +le_S_n: forall n m : nat, S n <= S m -> n <= m false: bool -andb: bool -> bool -> bool -orb: bool -> bool -> bool +true: bool +negb: bool -> bool implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool xorb: bool -> bool -> bool -negb: bool -> bool -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool Nat.even: nat -> bool Nat.odd: nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool -eq_S: forall x y : nat, x = y -> S x = S y -f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y +Nat.eqb: nat -> nat -> bool +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 pred_Sn: forall n : nat, n = Nat.pred (S n) +f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y 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 +eq_S: forall x y : nat, x = y -> S x = S y +max_r: forall n m : nat, n <= m -> Nat.max n m = m +max_l: forall n m : nat, m <= n -> Nat.max n m = n +min_r: forall n m : nat, m <= n -> Nat.min n m = m +min_l: forall n m : nat, n <= m -> Nat.min n m = 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) +mult_n_Sm: forall n m : nat, n * m + n = n * S m +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 -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 -> Nat.max n m = n -max_r: forall n m : nat, n <= m -> Nat.max n m = m -min_l: forall n m : nat, n <= m -> Nat.min n m = n -min_r: forall n m : nat, m <= n -> Nat.min n m = m h: newdef n h: P n diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out index f3c12effca..45ff5e73b6 100644 --- a/test-suite/output/SearchPattern.out +++ b/test-suite/output/SearchPattern.out @@ -1,77 +1,77 @@ -true: bool false: bool -andb: bool -> bool -> bool -orb: bool -> bool -> bool +true: bool +negb: bool -> bool implb: bool -> bool -> bool +orb: bool -> bool -> bool +andb: bool -> bool -> bool xorb: bool -> bool -> bool -negb: bool -> bool -Nat.eqb: nat -> nat -> bool -Nat.leb: nat -> nat -> bool -Nat.ltb: nat -> nat -> bool Nat.even: nat -> bool Nat.odd: nat -> bool +Nat.leb: nat -> nat -> bool +Nat.ltb: nat -> nat -> bool Nat.testbit: nat -> nat -> bool -O: nat -S: nat -> nat -length: forall A : Type, list A -> nat +Nat.eqb: nat -> nat -> bool +Nat.two: nat Nat.zero: nat Nat.one: nat -Nat.two: nat -Nat.succ: nat -> nat +O: nat +Nat.double: nat -> nat +Nat.sqrt: nat -> nat +Nat.div2: nat -> nat +Nat.log2: nat -> nat Nat.pred: nat -> nat +Nat.square: nat -> nat +S: nat -> nat +Nat.succ: nat -> nat +Nat.ldiff: nat -> nat -> nat Nat.add: nat -> nat -> nat -Nat.double: nat -> nat +Nat.lor: nat -> nat -> nat +Nat.lxor: nat -> nat -> nat +Nat.land: nat -> nat -> nat Nat.mul: nat -> nat -> nat Nat.sub: nat -> nat -> nat Nat.max: nat -> nat -> nat -Nat.min: nat -> nat -> nat -Nat.pow: nat -> nat -> nat Nat.div: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.min: nat -> nat -> nat Nat.modulo: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.square: nat -> nat Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat -Nat.sqrt: nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -Nat.log2: nat -> nat -Nat.div2: nat -> nat +length: forall A : Type, list A -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -Nat.land: nat -> nat -> nat -Nat.lor: nat -> nat -> nat +Nat.div2: nat -> nat +Nat.sqrt: nat -> nat +Nat.log2: nat -> nat +Nat.double: nat -> nat +Nat.pred: nat -> nat +Nat.square: nat -> nat +Nat.succ: nat -> nat +S: nat -> nat Nat.ldiff: nat -> nat -> nat +Nat.pow: nat -> nat -> nat +Nat.land: nat -> nat -> nat Nat.lxor: nat -> nat -> nat -S: nat -> nat -Nat.succ: nat -> nat -Nat.pred: nat -> nat -Nat.add: nat -> nat -> nat -Nat.double: nat -> nat +Nat.div: nat -> nat -> nat Nat.mul: nat -> nat -> nat -Nat.sub: nat -> nat -> nat -Nat.max: nat -> nat -> nat Nat.min: nat -> nat -> nat -Nat.pow: nat -> nat -> nat -Nat.div: nat -> nat -> nat Nat.modulo: nat -> nat -> nat +Nat.sub: nat -> nat -> nat +Nat.lor: nat -> nat -> nat Nat.gcd: nat -> nat -> nat -Nat.square: nat -> nat -Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat -Nat.sqrt: nat -> nat +Nat.max: nat -> nat -> nat +Nat.add: nat -> nat -> nat Nat.log2_iter: nat -> nat -> nat -> nat -> nat -Nat.log2: nat -> nat -Nat.div2: nat -> nat +Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat -Nat.land: nat -> nat -> nat -Nat.lor: nat -> nat -> nat -Nat.ldiff: nat -> nat -> nat -Nat.lxor: nat -> nat -> nat mult_n_Sm: forall n m : nat, n * m + n = n * S m -identity_refl: forall (A : Type) (a : A), identity a a iff_refl: forall A : Prop, A <-> A +le_n: forall n : nat, n <= n +identity_refl: forall (A : Type) (a : A), identity a a eq_refl: forall (A : Type) (x : A), x = x Nat.divmod: nat -> nat -> nat -> nat -> nat * nat -le_n: forall n : nat, n <= n -pair: forall A B : Type, A -> B -> A * B conj: forall A B : Prop, A -> B -> A /\ B +pair: forall A B : Type, A -> B -> A * B Nat.divmod: nat -> nat -> nat -> nat -> nat * nat h: n <> newdef n h: n <> newdef n diff --git a/test-suite/output/ShowProof.out b/test-suite/output/ShowProof.out new file mode 100644 index 0000000000..2d4be8bce7 --- /dev/null +++ b/test-suite/output/ShowProof.out @@ -0,0 +1 @@ +(fun x : Type => conj I ?Goal) diff --git a/test-suite/output/ShowProof.v b/test-suite/output/ShowProof.v new file mode 100644 index 0000000000..73ecaf2200 --- /dev/null +++ b/test-suite/output/ShowProof.v @@ -0,0 +1,6 @@ +(* Was #4524 *) +Definition foo (x : Type) : True /\ True. +Proof. +split. +- exact I. + Show Proof. (* Was not finding an evar name at some time *) diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out new file mode 100644 index 0000000000..a5b55a9993 --- /dev/null +++ b/test-suite/output/auto.out @@ -0,0 +1,20 @@ +(* info auto: *) +simple apply or_intror (in core). + intro. + assumption. +Debug: (* debug auto: *) +Debug: * assumption. (*fail*) +Debug: * intro. (*fail*) +Debug: * simple apply or_intror (in core). (*success*) +Debug: ** assumption. (*fail*) +Debug: ** intro. (*success*) +Debug: ** assumption. (*success*) +(* info eauto: *) +simple apply or_intror. + intro. + exact H. +Debug: (* debug eauto: *) +Debug: 1 depth=5 +Debug: 1.1 depth=4 simple apply or_intror +Debug: 1.1.1 depth=4 intro +Debug: 1.1.1.1 depth=4 exact H diff --git a/test-suite/output/auto.v b/test-suite/output/auto.v new file mode 100644 index 0000000000..a77b7b82e6 --- /dev/null +++ b/test-suite/output/auto.v @@ -0,0 +1,11 @@ +(* testing info/debug auto/eauto *) + +Goal False \/ (True -> True). +info_auto. +Undo. +debug auto. +Undo. +info_eauto. +Undo. +debug eauto. +Qed. diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 1ff09e3af6..35c3057d84 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,5 +1,4 @@ The command has indeed failed with message: -Error: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize @@ -22,11 +21,11 @@ The term "I" has type "True" while it is expected to have type "False". The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. -Error: No primitive equality found. +No primitive equality found. The command has indeed failed with message: In nested Ltac calls to "h" and "injection (destruction_arg)", last call failed. -Error: No primitive equality found. +No primitive equality found. Hx nat nat diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out new file mode 100644 index 0000000000..172612405f --- /dev/null +++ b/test-suite/output/ltac_missing_args.out @@ -0,0 +1,20 @@ +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing arguments for variables y and _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable _. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. +The command has indeed failed with message: +A fully applied tactic is expected: missing argument for variable x. diff --git a/test-suite/output/ltac_missing_args.v b/test-suite/output/ltac_missing_args.v new file mode 100644 index 0000000000..8ecd97aa56 --- /dev/null +++ b/test-suite/output/ltac_missing_args.v @@ -0,0 +1,19 @@ +Ltac foo x := idtac x. +Ltac bar x := fun y _ => idtac x y. +Ltac baz := foo. +Ltac qux := bar. +Ltac mydo tac := tac (). +Ltac rec x := rec. + +Goal True. + Fail foo. + Fail bar. + Fail bar True. + Fail baz. + Fail qux. + Fail mydo ltac:(fun _ _ => idtac). + Fail let tac := (fun _ => idtac) in tac. + Fail (fun _ => idtac). + Fail rec True. + Fail let rec tac x := tac in tac True. +Abort.
\ No newline at end of file |