aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_032.v
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-06-15 13:24:41 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-06-15 13:24:41 +0200
commit0a51137f7ff80afdcf216d85cd8be25a531bc39b (patch)
treeb8ce1197001e7d387c42bc48ae155313d0ec6956 /test-suite/bugs/closed/HoTT_coq_032.v
parentdf6e64fd28e9ba8b12045768869c7f083a15e9c0 (diff)
- Fix xml plugin treatment of inductives.
- Move HoTT bug #30 to closed
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_032.v')
-rw-r--r--test-suite/bugs/closed/HoTT_coq_032.v22
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 000000000..3f5d7b021
--- /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. *)