diff options
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 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. |