diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-13 17:36:16 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-13 17:51:34 +0100 |
| commit | 97e1fccd878190a1fc51a1da45f4c06369c0e3db (patch) | |
| tree | 27e38c1ae4c8ebef7dc7f8f893ccc8f93aee8227 /test-suite/success | |
| parent | e9675e068f9e0e92bab05c030fb4722b146123b8 (diff) | |
| parent | f46a5686853353f8de733ae7fbd21a3a61977bc7 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/Injection.v | 2 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 2 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 8 |
3 files changed, 6 insertions, 6 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 8fd039462..56ed89ed8 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -70,7 +70,7 @@ Abort. Goal (forall x y : nat, x = y -> S x = S y) -> True. intros. -einjection (H O) as H0. +einjection (H O ?[y]) as H0. instantiate (y:=O). Abort. diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 55b666b72..02e043bc3 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -543,7 +543,7 @@ Qed. Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a): exists x, exists y, X x y. Proof. -intros; eexists; eexists; case H. +intros; eexists; eexists ?[y]; case H. apply (foo ?y). Grab Existential Variables. exact 0. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 9f091e399..90a60daa6 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -96,21 +96,21 @@ Abort. (* Check that subterm selection does not solve existing evars *) Goal exists x, S x = S 0. -eexists. +eexists ?[x]. Show x. (* Incidentally test Show on a named goal *) destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S 0). Abort. Goal exists x, S 0 = S x. -eexists. +eexists ?[x]. destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) change (0 = S ?x). [x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *) Abort. Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. -do 2 eexists. +eexists ?[n]; eexists ?[p]. destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *) change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n). Abort. @@ -426,7 +426,7 @@ destruct b eqn:H. (* Check natural instantiation behavior when the goal has already an evar *) Goal exists x, S x = x. -eexists. +eexists ?[x]. destruct (S _). change (0 = ?x). Abort. |