Imported Upstream version 8.5~beta1+dfsg

1 files changed, 22 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v
new file mode 100644
index 00000000..3f5d7b02
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_032.v
@@ -0,0 +1,22 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-xml") -*- *)
+Set Implicit Arguments.
+Generalizable All Variables.
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+
+Delimit Scope object_scope with object.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope functor_scope with functor.
+
+Local Open Scope category_scope.
+
+Record SpecializedCategory (obj : Type) :=
+  {
+    Object :> _ := obj;
+    Morphism : obj -> obj -> Type;
+
+    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+  }.
+(* Anomaly: Mismatched instance and context when building universe substitution.
+Please report. *)