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/HoTT_coq_102.v | 29 +++++++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 test-suite/bugs/closed/HoTT_coq_102.v (limited to 'test-suite/bugs/closed/HoTT_coq_102.v') diff --git a/test-suite/bugs/closed/HoTT_coq_102.v b/test-suite/bugs/closed/HoTT_coq_102.v new file mode 100644 index 00000000..71becfd2 --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_102.v @@ -0,0 +1,29 @@ +(* File reduced by coq-bug-finder from 64 lines to 30 lines. *) +Set Implicit Arguments. +Set Universe Polymorphism. +Generalizable All Variables. +Record SpecializedCategory (obj : Type) := { Object :> _ := obj }. + +Record > Category := + { CObject : Type; + UnderlyingCategory :> @SpecializedCategory CObject }. + +Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) := + { ObjectOf :> objC -> objD }. + +Definition Functor (C D : Category) := SpecializedFunctor C D. + +Parameter TerminalCategory : SpecializedCategory unit. + +Definition focus A (_ : A) := True. + +Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type. + assert (Hf : focus ((S tt) = (S tt))) by constructor. + let C1 := constr:(CObject) in + let C2 := constr:(fun C => @Object (CObject C) C) in + let check := constr:(eq_refl : C1 = C2) in + unify C1 C2. + progress change CObject with (fun C => @Object (CObject C) C) in *. + (* not convertible *) + admit. +Defined. -- cgit v1.2.3