diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-15 10:51:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-15 14:42:29 +0100 |
| commit | cedcfc9bc386456f3fdd225f739706e4f7a2902c (patch) | |
| tree | c8161338a95bebdab6501606edda5a0a939da4a0 /test-suite/bugs/closed/3699.v | |
| parent | 8b15e47a6b3ccae696da8e12dbad81ae0a740782 (diff) | |
Refine tactic now shelves unifiable holes.
The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
Diffstat (limited to 'test-suite/bugs/closed/3699.v')
| -rw-r--r-- | test-suite/bugs/closed/3699.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index 62137f0c0..aad0bb44d 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -34,8 +34,8 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intro x. exact (transport P x.2 (d x.1)). Defined. @@ -47,8 +47,8 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intros [a p]. exact (transport P p (d a)). Defined. @@ -111,8 +111,8 @@ Module Prim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intro x. exact (transport P x.2 (d x.1)). Defined. @@ -124,8 +124,8 @@ Module Prim. : forall b:B, P b. Proof. intros b. - refine (pr1 (isconnected_elim _ _)). - 2:exact b. + unshelve (refine (pr1 (isconnected_elim _ _))). + exact b. intros [a p]. exact (transport P p (d a)). Defined. |