diff options
| author | Pierre-Marie Pédrot | 2015-12-15 10:51:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-15 14:42:29 +0100 |
| commit | cedcfc9bc386456f3fdd225f739706e4f7a2902c (patch) | |
| tree | c8161338a95bebdab6501606edda5a0a939da4a0 /test-suite/bugs | |
| 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')
| -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 a5bea34a98..7a0c3e6f1d 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 b650920b26..df5f667480 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 62137f0c06..aad0bb44d5 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. |