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 | |
| 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')
| -rw-r--r-- | test-suite/bugs/closed/3685.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3686.v | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/3699.v | 16 |
3 files changed, 12 insertions, 12 deletions
diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v index a5bea34a9..7a0c3e6f1 100644 --- a/test-suite/bugs/closed/3685.v +++ b/test-suite/bugs/closed/3685.v @@ -39,11 +39,11 @@ Module Export PointwiseCore. (G : Functor D D') : Functor (C -> D) (C' -> D'). Proof. - refine (Build_Functor + unshelve (refine (Build_Functor (C -> D) (C' -> D') _ _ - _); + _)); abstract admit. Defined. End PointwiseCore. diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v index b650920b2..df5f66748 100644 --- a/test-suite/bugs/closed/3686.v +++ b/test-suite/bugs/closed/3686.v @@ -33,11 +33,11 @@ Module Export PointwiseCore. (G : Functor D D') : Functor (C -> D) (C' -> D'). Proof. - refine (Build_Functor + unshelve (refine (Build_Functor (C -> D) (C' -> D') _ _ - _); + _)); abstract admit. Defined. End PointwiseCore. 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. |