diff options
Diffstat (limited to 'test-suite/bugs/closed/3424.v')
| -rw-r--r-- | test-suite/bugs/closed/3424.v | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/test-suite/bugs/closed/3424.v b/test-suite/bugs/closed/3424.v deleted file mode 100644 index ee8cabf1..00000000 --- a/test-suite/bugs/closed/3424.v +++ /dev/null @@ -1,24 +0,0 @@ -Set Universe Polymorphism. -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Class Contr_internal (A : Type) := BuildContr { center : A ; contr : (forall y : A, center = y) }. -Inductive trunc_index : Type := minus_two | trunc_S (x : trunc_index). -Bind Scope trunc_scope with trunc_index. -Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type := - match n with - | minus_two => Contr_internal A - | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y) - end. -Notation minus_one:=(trunc_S minus_two). -Notation "0" := (trunc_S minus_one) : trunc_scope. -Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. -Notation IsHProp := (IsTrunc minus_one). -Notation IsHSet := (IsTrunc 0). -Set Refolding Reduction. -Goal forall (A : Type) (a b : A) (H' : IsHSet A), { x : Type & IsHProp x }. -Proof. -intros. -eexists. -(* exact (H' a b). *) -(* Undo. *) -apply (H' a b). -Qed. |