diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-29 12:37:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-11-03 16:26:40 +0100 |
| commit | d51c384e52003668bd97ca44da77a14c91e5cb14 (patch) | |
| tree | de591c962766ca0d826bec7620a35b41aa2730c7 /test-suite/bugs/closed/3699.v | |
| parent | 0ab187ee578f0ef49ecf484278b8d3569630ee48 (diff) | |
Fix test-suite files relying on tcs bugs
- One was expecting shelved goals to remain after resolution (from refine).
- The other too were relying on the wrong classification of subgoals
as typeclass subgoals at toplevel.
Diffstat (limited to 'test-suite/bugs/closed/3699.v')
| -rw-r--r-- | test-suite/bugs/closed/3699.v | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index 8dadc2419..efa432526 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -34,8 +34,7 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intro x. exact (transport P x.2 (d x.1)). Defined. @@ -47,8 +46,7 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intros [a p]. exact (transport P p (d a)). Defined. @@ -111,8 +109,7 @@ Module Prim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intro x. exact (transport P x.2 (d x.1)). Defined. @@ -124,8 +121,7 @@ Module Prim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intros [a p]. exact (transport P p (d a)). Defined. |