diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_107.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_107.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v index c3a83627e..9a1da16bf 100644 --- a/test-suite/bugs/closed/HoTT_coq_107.v +++ b/test-suite/bugs/closed/HoTT_coq_107.v @@ -59,7 +59,7 @@ Instance trunc_sigma `{P : A -> Type} Proof. generalize dependent A. - induction n; [ | admit ]; simpl; intros A P ac Pc. + induction n; [ | apply admit ]; simpl; intros A P ac Pc. (exists (existT _ (center A) (center (P (center A))))). intros [a ?]. refine (path_sigma' P (contr a) (path_contr _ _)). @@ -102,5 +102,5 @@ The term | false => B end))" (Universe inconsistency: Cannot enforce Top.197 = Set)). *) - admit. + apply admit. Defined. |