From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/3331.v | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 test-suite/bugs/closed/3331.v (limited to 'test-suite/bugs/closed/3331.v') diff --git a/test-suite/bugs/closed/3331.v b/test-suite/bugs/closed/3331.v new file mode 100644 index 00000000..9cd44bd0 --- /dev/null +++ b/test-suite/bugs/closed/3331.v @@ -0,0 +1,31 @@ +(* File reduced by coq-bug-finder from original input, then from 6303 lines to 66 lines, then from 63 lines to 36 lines *) +Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y :> A" := (@paths A x y) : type_scope. +Arguments idpath {A a} , [A] a. +Notation "x = y" := (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_index +| trunc_S : trunc_index -> 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. +Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A. +Instance istrunc_paths (A : Type) n `{H : IsTrunc (trunc_S n) A} (x y : A) : IsTrunc n (x = y) := H x y. +Notation Contr := (IsTrunc minus_two). +Section groupoid_category. + Variable X : Type. + Context `{H : IsTrunc (trunc_S (trunc_S (trunc_S minus_two))) X}. + Goal X -> True. + intro d. + pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))) as H'. (* success *) + clear H'. + compute in H. + change (forall (x y : X) (p q : x = y) (r s : p = q), Contr (r = s)) in H. + assert (H' := H). + set (foo:=_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). (* success *) + clear H' foo. + Set Typeclasses Debug. + pose (_ : Contr (idpath = idpath :> (@paths (@paths X d d) idpath idpath))). +Abort. \ No newline at end of file -- cgit v1.2.3