diff options
Diffstat (limited to 'test-suite')
29 files changed, 455 insertions, 91 deletions
diff --git a/test-suite/bugs/closed/2245.v b/test-suite/bugs/closed/2245.v new file mode 100644 index 000000000..f0162f3b2 --- /dev/null +++ b/test-suite/bugs/closed/2245.v @@ -0,0 +1,11 @@ +Module Type Test. + +Section Sec. +Variables (A:Type). +Context (B:Type). +End Sec. + +Fail Check B. (* used to be found !!! *) +Fail Check A. + +End Test. diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v index 85ad41d1c..23a58501f 100644 --- a/test-suite/bugs/closed/2378.v +++ b/test-suite/bugs/closed/2378.v @@ -505,8 +505,6 @@ Qed. Require Export Coq.Logic.FunctionalExtensionality. Print PLanguage. -Unset Standard Proposition Elimination Names. - Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): Transformation (PLanguage l1) (PLanguage l2) := mkTransformation (PLanguage l1) (PLanguage l2) diff --git a/test-suite/bugs/closed/3481.v b/test-suite/bugs/closed/3481.v index 89d476dcb..38f03b166 100644 --- a/test-suite/bugs/closed/3481.v +++ b/test-suite/bugs/closed/3481.v @@ -3,7 +3,7 @@ Set Implicit Arguments. Require Import Logic. Module NonPrim. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Record prodwithlet (A B : Type) : Type := pair' { fst : A; fst' := fst; snd : B }. @@ -21,7 +21,7 @@ End NonPrim. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Local Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 5adc48215..1f0f3b0da 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -69,26 +69,6 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) refine (P _ _) end; unfold Basics.flip. Focus 2. - Set Typeclasses Debug. - Set Typeclasses Legacy Resolution. - apply reflexivity. - (* Debug: 1.1: apply @IsPointed_catOP on -(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0)) -Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0)) -Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x)) -Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails) -Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities -Debug: Backtracking after apply @Equivalence_Reflexive -Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails) -Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails) -Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) -*) - Undo. Unset Typeclasses Legacy Resolution. - Test Typeclasses Unique Solutions. - Test Typeclasses Unique Instances. - Show Existentials. - Set Typeclasses Debug Verbosity 2. - Set Printing All. (* As in 8.5, allow a shelved subgoal to remain *) apply reflexivity. diff --git a/test-suite/bugs/closed/3520.v b/test-suite/bugs/closed/3520.v index c981207e6..ea122e521 100644 --- a/test-suite/bugs/closed/3520.v +++ b/test-suite/bugs/closed/3520.v @@ -3,7 +3,7 @@ Set Primitive Projections. Record foo (A : Type) := { bar : Type ; baz := Set; bad : baz = bar }. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record notprim : Prop := { irrel : True; relevant : nat }. diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v index bd53389b4..b8754bce9 100644 --- a/test-suite/bugs/closed/3662.v +++ b/test-suite/bugs/closed/3662.v @@ -1,6 +1,6 @@ Set Primitive Projections. Set Implicit Arguments. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record prod A B := pair { fst : A ; snd : B }. Definition f : Set -> Type := fun x => x. diff --git a/test-suite/bugs/closed/6313.v b/test-suite/bugs/closed/6313.v new file mode 100644 index 000000000..4d263c5a8 --- /dev/null +++ b/test-suite/bugs/closed/6313.v @@ -0,0 +1,64 @@ +(* Former open goals in nested proofs were lost *) + +(* This used to fail with "Incorrect number of goals (expected 1 tactic)." *) + +Inductive foo := a | b | c. +Goal foo -> foo. + intro x. + simple refine (match x with + | a => _ + | b => ltac:(exact b) + | c => _ + end); [exact a|exact c]. +Abort. + +(* This used to leave the goal on the shelf and fails at reflexivity *) + +Goal (True/\0=0 -> True) -> True. + intro f. + refine + (f ltac:(split; only 1:exact I)). + reflexivity. +Qed. + +(* The "Unshelve" used to not see the explicitly "shelved" goal *) + +Lemma f (b:comparison) : b=b. +refine (match b with + Eq => ltac:(shelve) + | Lt => ltac:(give_up) + | Gt => _ + end). +exact (eq_refl Gt). +Unshelve. +exact (eq_refl Eq). +Fail auto. (* Check that there are no more regular subgoals *) +Admitted. + +(* The "Unshelve" used to not see the explicitly "shelved" goal *) + +Lemma f2 (b:comparison) : b=b. +refine (match b with + Eq => ltac:(shelve) + | Lt => ltac:(give_up) + | Gt => _ + end). +Unshelve. (* Note: Unshelve puts goals at the end *) +exact (eq_refl Gt). +exact (eq_refl Eq). +Fail auto. (* Check that there are no more regular subgoals *) +Admitted. + +(* The "unshelve" used to not see the explicitly "shelved" goal *) + +Lemma f3 (b:comparison) : b=b. +unshelve refine (match b with + Eq => ltac:(shelve) + | Lt => ltac:(give_up) + | Gt => _ + end). +(* Note: unshelve puts goals at the beginning *) +exact (eq_refl Eq). +exact (eq_refl Gt). +Fail auto. (* Check that there are no more regular subgoals *) +Admitted. diff --git a/test-suite/bugs/closed/6634.v b/test-suite/bugs/closed/6634.v new file mode 100644 index 000000000..7f33afcc2 --- /dev/null +++ b/test-suite/bugs/closed/6634.v @@ -0,0 +1,6 @@ +From Coq Require Import ssreflect. + +Lemma normalizeP (p : tt = tt) : p = p. +Proof. +Fail move: {2} tt p. +Abort. diff --git a/test-suite/bugs/closed/6910.v b/test-suite/bugs/closed/6910.v new file mode 100644 index 000000000..5167a5364 --- /dev/null +++ b/test-suite/bugs/closed/6910.v @@ -0,0 +1,5 @@ +From Coq Require Import ssreflect ssrfun. + +(* We should be able to use Some_inj as a view: *) +Lemma foo (x y : nat) : Some x = Some y -> x = y. +Proof. by move/Some_inj. Qed. diff --git a/test-suite/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v index 017780c1f..f69c71a02 100644 --- a/test-suite/bugs/closed/HoTT_coq_077.v +++ b/test-suite/bugs/closed/HoTT_coq_077.v @@ -3,7 +3,7 @@ Set Implicit Arguments. Require Import Logic. Set Asymmetric Patterns. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v index 5bb7fa8c1..a6ff78d12 100644 --- a/test-suite/bugs/closed/HoTT_coq_104.v +++ b/test-suite/bugs/closed/HoTT_coq_104.v @@ -4,7 +4,7 @@ Require Import Logic. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Local Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/opened/1596.v b/test-suite/bugs/opened/1596.v index 0b576db6b..820022d99 100644 --- a/test-suite/bugs/opened/1596.v +++ b/test-suite/bugs/opened/1596.v @@ -2,7 +2,6 @@ Require Import Relations. Require Import FSets. Require Import Arith. Require Import Omega. -Unset Standard Proposition Elimination Names. Set Keyed Unification. diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v deleted file mode 100644 index cfad76357..000000000 --- a/test-suite/bugs/opened/3926.v +++ /dev/null @@ -1,30 +0,0 @@ -Notation compose := (fun g f x => g (f x)). -Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. -Open Scope function_scope. -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Arguments idpath {A a} , [A] a. -Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. -Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }. -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. -Local Open Scope equiv_scope. -Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x. -Generalizable Variables A B C f g. -Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000 - := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1). -Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g - := Build_IsEquiv _ _ g (f ^-1). -Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000 - := Build_IsEquiv B A f^-1 f. -Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} - `{IsEquiv A B f} `{IsEquiv A C (g o f)} - : IsEquiv g. -Proof. - Unset Typeclasses Modulo Eta. - exact (isequiv_homotopic (compose (compose g f) f^-1) - (fun b => ap g (eisretr f b))) || fail "too early". - Undo. - Set Typeclasses Modulo Eta. - Set Typeclasses Dependency Order. - Set Typeclasses Debug. - Fail exact (isequiv_homotopic (compose (compose g f) f^-1) - (fun b => ap g (eisretr f b))). diff --git a/test-suite/failure/fixpointeta.v b/test-suite/failure/fixpointeta.v new file mode 100644 index 000000000..9af719322 --- /dev/null +++ b/test-suite/failure/fixpointeta.v @@ -0,0 +1,70 @@ + +Set Primitive Projections. + +Record R := C { p : nat }. +(* R is defined +p is defined *) + +Unset Primitive Projections. +Record R' := C' { p' : nat }. + + + +Fail Definition f := fix f (x : R) : nat := p x. +(** Not allowed to make fixpoint defs on (non-recursive) records + having eta *) + +Fail Definition f := fix f (x : R') : nat := p' x. +(** Even without eta (R' is not primitive here), as long as they're + found to be BiFinite (non-recursive), we disallow it *) + +(* + +(* Subject reduction failure example, if we allowed fixpoints *) + +Set Primitive Projections. + +Record R := C { p : nat }. + +Definition f := fix f (x : R) : nat := p x. + +(* eta rule for R *) +Definition Rtr (P : R -> Type) x (v : P (C (p x))) : P x + := v. + +Definition goal := forall x, f x = p x. + +(* when we compute the Rtr away typechecking will fail *) +Definition thing : goal := fun x => +(Rtr (fun x => f x = p x) x (eq_refl _)). + +Definition thing' := Eval compute in thing. + +Fail Check (thing = thing'). +(* +The command has indeed failed with message: +The term "thing'" has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +while it is expected to have type "goal" (cannot unify "(let (p) := x in p) = (let (p) := x in p)" +and "f x = p x"). +*) + +Definition thing_refl := eq_refl thing. + +Fail Definition thing_refl' := Eval compute in thing_refl. +(* +The command has indeed failed with message: +Illegal application: +The term "@eq_refl" of type "forall (A : Type) (x : A), x = x" +cannot be applied to the terms + "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)" : "Prop" + "fun x : R => eq_refl" : "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +The 2nd term has type "forall x : R, (let (p) := x in p) = (let (p) := x in p)" +which should be coercible to + "forall x : R, (fix f (x0 : R) : nat := let (p) := x0 in p) x = (let (p) := x in p)". + *) + +Definition more_refls : thing_refl = thing_refl. +Proof. + compute. reflexivity. +Fail Defined. Abort. + *) diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index abf8be72e..d163dfbcd 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -40,7 +40,7 @@ Proof. Qed. -Lemma QdenZpower : forall x : Q, ' Qden (x ^ 2)%Q = ('(Qden x) ^ 2) %Z. +Lemma QdenZpower : forall x : Q, Zpos (Qden (x ^ 2)%Q) = (Zpos (Qden x) ^ 2) %Z. Proof. intros. destruct x. @@ -54,9 +54,9 @@ Qed. Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. unfold Qeq; intros (x,HQeq); simpl (Qden (2#1)) in HQeq; rewrite Z.mul_1_r in HQeq. - assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by + assert (Heq : (Qnum x ^ 2 = 2 * Zpos (Qden x) ^ 2%Q)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). assert (Hnx : (Qnum x <> 0)%Z) by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq). - apply integer_statement; exists (Qnum x); exists (' Qden x); auto. + apply integer_statement; exists (Qnum x); exists (Zpos (Qden x)); auto. Qed. diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v new file mode 100644 index 000000000..e68345516 --- /dev/null +++ b/test-suite/modules/WithDefUBinders.v @@ -0,0 +1,15 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo@{u v|u < v} : Type@{v}. +End T. + +Module M : T with Definition foo@{u v} := Type@{u} : Type@{v}. + Definition foo@{u v} := Type@{u} : Type@{v}. +End M. + +Fail Module M' : T with Definition foo := Type. + +(* Without the binder expression we have to do trickery to get the + universes in the right order. *) +Module M' : T with Definition foo := let t := Type in t. diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out index 4df21ae35..e73312c67 100644 --- a/test-suite/output/Arguments_renaming.out +++ b/test-suite/output/Arguments_renaming.out @@ -11,7 +11,7 @@ notation scopes add ': clear scopes' [arguments-assert,vernacular] eq_refl : ?y = ?y where -?y : [ |- nat] +?y : [ |- nat] Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x For eq_refl: Arguments are renamed to B, y diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out index 9680d2bbf..18f5d89f6 100644 --- a/test-suite/output/Existentials.out +++ b/test-suite/output/Existentials.out @@ -1,4 +1,4 @@ -Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m] +Existential 1 = ?Goal : [p : nat q := S p : nat n : nat m : nat |- ?y = m] Existential 2 = -?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) -Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] +?y : [p : nat q := S p : nat n : nat m : nat |- nat] (p, q cannot be used) (shelved) +Existential 3 = ?Goal0 : [q : nat n : nat m : nat |- n = ?y] diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index e6a6e0288..864b6151a 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -33,24 +33,24 @@ fun f : forall x : nat * (bool * unit), ?T => CURRY (x : nat) (y : bool), f : (forall x : nat * (bool * unit), ?T) -> forall (x : nat) (y : bool), ?T@{x:=(x, (y, tt))} where -?T : [x : nat * (bool * unit) |- Type] +?T : [x : nat * (bool * unit) |- Type] fun f : forall x : bool * (nat * unit), ?T => CURRYINV (x : nat) (y : bool), f : (forall x : bool * (nat * unit), ?T) -> forall (x : nat) (y : bool), ?T@{x:=(y, (x, tt))} where -?T : [x : bool * (nat * unit) |- Type] +?T : [x : bool * (nat * unit) |- Type] fun f : forall x : unit * nat * bool, ?T => CURRYLEFT (x : nat) (y : bool), f : (forall x : unit * nat * bool, ?T) -> forall (x : nat) (y : bool), ?T@{x:=(tt, x, y)} where -?T : [x : unit * nat * bool |- Type] +?T : [x : unit * nat * bool |- Type] fun f : forall x : unit * bool * nat, ?T => CURRYINVLEFT (x : nat) (y : bool), f : (forall x : unit * bool * nat, ?T) -> forall (x : nat) (y : bool), ?T@{x:=(tt, y, x)} where -?T : [x : unit * bool * nat |- Type] +?T : [x : unit * bool * nat |- Type] forall n : nat, {#n | 1 > n} : Prop forall x : nat, {|x | x > 0|} diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out index d28ee4276..5e9eff048 100644 --- a/test-suite/output/inference.out +++ b/test-suite/output/inference.out @@ -9,10 +9,10 @@ fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H fun n : nat => let y : T n := A n in ?t ?x : T n : forall n : nat, T n where -?t : [n : nat y := A n : T n |- ?T -> T n] -?x : [n : nat y := A n : T n |- ?T] +?t : [n : nat y := A n : T n |- ?T -> T n] +?x : [n : nat y := A n : T n |- ?T] fun n : nat => ?t ?x : T n : forall n : nat, T n where -?t : [n : nat |- ?T -> T n] -?x : [n : nat |- ?T] +?t : [n : nat |- ?T -> T n] +?x : [n : nat |- ?T] diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 6962e43e7..8d08f5975 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -172,3 +172,14 @@ Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e) Timeout 1 Fail apply _. (* 0.06s *) Abort. End HintCut. + + +(* Check that auto-like tactics do not prefer "eq_refl" over more complex solutions, *) +(* e.g. those tactics when considering a goal with existential varibles *) +(* like "m = ?n" won't pick "plus_n_O" hint over "eq_refl" hint. *) +(* See this Coq club post for more detail: *) +(* https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00103.html *) + +Goal forall (m : nat), exists n, m = n /\ m = n. + intros m; eexists; split; [trivial | reflexivity]. +Qed. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 893d75b77..5b1482fd5 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -200,3 +200,9 @@ Module NonRecLetIn. (fun n b c => f_equal (Rec n) eq_refl) 0 (Rec 0 (Base 1)). End NonRecLetIn. + +(* Test treatment of let-in in the definition of Records *) +(* Should fail with "Sort expected" *) + +Fail Inductive foo (T : Type) : let T := Type in T := + { r : forall x : T, x = x }. diff --git a/test-suite/success/ShowExtraction.v b/test-suite/success/ShowExtraction.v new file mode 100644 index 000000000..e34c240c5 --- /dev/null +++ b/test-suite/success/ShowExtraction.v @@ -0,0 +1,31 @@ + +Require Extraction. +Require Import List. + +Section Test. +Variable A : Type. +Variable decA : forall (x y:A), {x=y}+{x<>y}. + +(** Should fail when no proofs are started *) +Fail Show Extraction. + +Lemma decListA : forall (xs ys : list A), {xs=ys}+{xs<>ys}. +Proof. +Show Extraction. +fix 1. +destruct xs as [|x xs], ys as [|y ys]. +Show Extraction. +- now left. +- now right. +- now right. +- Show Extraction. + destruct (decA x y). + + destruct (decListA xs ys). + * left; now f_equal. + * Show Extraction. + right. congruence. + + right. congruence. +Show Extraction. +Defined. + +End Test. diff --git a/test-suite/success/cumulativity.v b/test-suite/success/cumulativity.v index e05762477..4dda36042 100644 --- a/test-suite/success/cumulativity.v +++ b/test-suite/success/cumulativity.v @@ -134,3 +134,24 @@ Definition withparams_co@{i i' j|i < i', i' < j} : withparams@{i j} -> withparam Fail Definition withparams_not_irr@{i i' j|i' < i, i' < j} : withparams@{i j} -> withparams@{i' j} := fun x => x. + +(** Cumulative constructors *) + + +Record twotys@{u v w} : Type@{w} := + twoconstr { fstty : Type@{u}; sndty : Type@{v} }. + +Monomorphic Universes i j k l. + +Monomorphic Constraint i < j. +Monomorphic Constraint j < k. +Monomorphic Constraint k < l. + +Parameter Tyi : Type@{i}. + +Definition checkcumul := + eq_refl _ : @eq twotys@{k k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi). + +(* They can only be compared at the highest type *) +Fail Definition checkcumul' := + eq_refl _ : @eq twotys@{i k l} (twoconstr@{i j k} Tyi Tyi) (twoconstr@{j i k} Tyi Tyi). diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v index a183be622..de2857b43 100644 --- a/test-suite/success/letproj.v +++ b/test-suite/success/letproj.v @@ -1,5 +1,5 @@ Set Primitive Projections. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record Foo (A : Type) := { bar : A -> A; baz : A }. Definition test (A : Type) (f : Foo A) := diff --git a/test-suite/success/name_mangling.v b/test-suite/success/name_mangling.v new file mode 100644 index 000000000..571dde880 --- /dev/null +++ b/test-suite/success/name_mangling.v @@ -0,0 +1,192 @@ +(* -*- coq-prog-args: ("-mangle-names" "_") -*- *) + +(* Check that refine policy of redefining previous names make these names private *) +(* abstract can change names in the environment! See bug #3146 *) + +Goal True -> True. +intro. +Fail exact H. +exact _0. +Abort. + +Unset Mangle Names. +Goal True -> True. +intro; exact H. +Abort. + +Set Mangle Names. +Set Mangle Names Prefix "baz". +Goal True -> True. +intro. +Fail exact H. +Fail exact _0. +exact baz0. +Abort. + +Goal True -> True. +intro; assumption. +Abort. + +Goal True -> True. +intro x; exact x. +Abort. + +Goal forall x y, x+y=0. +intro x. +refine (fun x => _). +Fail Check x0. +Check x. +Abort. + +(* Example from Emilio *) + +Goal forall b : False, b = b. +intro b. +refine (let b := I in _). +Fail destruct b0. +Abort. + +(* Example from Cyprien *) + +Goal True -> True. +Proof. + refine (fun _ => _). + Fail exact t. +Abort. + +(* Example from Jason *) + +Goal False -> False. +intro H. +Fail abstract exact H. +Abort. + +(* Variant *) + +Goal False -> False. +intro. +Fail abstract exact H. +Abort. + +(* Example from Jason *) + +Goal False -> False. +intro H. +(* Name H' is from Ltac here, so it preserves the privacy *) +(* But abstract messes everything up *) +Fail let H' := H in abstract exact H'. +let H' := H in exact H'. +Qed. + +(* Variant *) + +Goal False -> False. +intro. +Fail let H' := H in abstract exact H'. +Abort. + +(* Indirectly testing preservation of names by move (derived from Jason) *) + +Inductive nat2 := S2 (_ _ : nat2). +Goal forall t : nat2, True. + intro t. + let IHt1 := fresh "IHt1" in + let IHt2 := fresh "IHt2" in + induction t as [? IHt1 ? IHt2]. + Fail exact IHt1. +Abort. + +(* Example on "pose proof" (from Jason) *) + +Goal False -> False. +intro; pose proof I as H0. +Fail exact H. +Abort. + +(* Testing the approach for which non alpha-renamed quantified names are user-generated *) + +Section foo. +Context (b : True). +Goal forall b : False, b = b. +Fail destruct b0. +Abort. + +Goal forall b : False, b = b. +now destruct b. +Qed. +End foo. + +(* Test stability of "fix" *) + +Lemma a : forall n, n = 0. +Proof. +fix a 1. +Check a. +fix 1. +Fail Check a0. +Abort. + +(* Test stability of "induction" *) + +Lemma a : forall n : nat, n = n. +Proof. +intro n; induction n as [ | n IHn ]. +- auto. +- Check n. + Check IHn. +Abort. + +Inductive I := C : I -> I -> I. + +Lemma a : forall n : I, n = n. +Proof. +intro n; induction n as [ n1 IHn1 n2 IHn2 ]. +Check n1. +Check n2. +apply f_equal2. ++ apply IHn1. ++ apply IHn2. +Qed. + +(* Testing remember *) + +Lemma c : 0 = 0. +Proof. +remember 0 as x eqn:Heqx. +Check Heqx. +Abort. + +Lemma c : forall Heqx, Heqx -> 0 = 0. +Proof. +intros Heqx X. +remember 0 as x. +Fail Check Heqx0. (* Heqx0 is not canonical *) +Abort. + +(* An example by Jason from the discussion for PR #268 *) + +Goal nat -> Set -> True. + intros x y. + match goal with + | [ x : _, y : _ |- _ ] + => let z := fresh "z" in + rename y into z, x into y; + let x' := fresh "x" in + rename z into x' + end. + revert y. (* x has been explicitly moved to y *) + Fail revert x. (* x comes from "fresh" *) +Abort. + +Goal nat -> Set -> True. + intros. + match goal with + | [ x : _, y : _ |- _ ] + => let z := fresh "z" in + rename y into z, x into y; + let x' := fresh "x" in + rename z into x' + end. + Fail revert y. (* generated by intros *) + Fail revert x. (* generated by intros *) +Abort. diff --git a/test-suite/success/old_typeclass.v b/test-suite/success/old_typeclass.v deleted file mode 100644 index 01e35810b..000000000 --- a/test-suite/success/old_typeclass.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import Setoid Coq.Classes.Morphisms. -Set Typeclasses Legacy Resolution. - -Declare Instance and_Proper_eq: Proper (Logic.eq ==> Logic.eq ==> Logic.eq) and. - -Axiom In : Prop. -Axiom union_spec : In <-> True. - -Lemma foo : In /\ True. -Proof. -progress rewrite union_spec. -repeat constructor. -Qed. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 576bdbf71..31a1608c4 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -1,5 +1,5 @@ Set Primitive Projections. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Module Prim. Record F := { a : nat; b : a = a }. diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v index 3f6b9cb39..916bb846a 100644 --- a/test-suite/success/shrink_abstract.v +++ b/test-suite/success/shrink_abstract.v @@ -1,5 +1,3 @@ -Set Shrink Abstract. - Definition foo : forall (n m : nat), bool. Proof. pose (p := 0). |