aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_032.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2014-05-09 10:13:32 -0400
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-10 15:39:39 +0200
commitc7284415e4bdd3315c84c7d15d140d3fee000bc5 (patch)
treecc8ded3feba7e1da0dd4f7d17b7e5f974de752c3 /test-suite/bugs/closed/HoTT_coq_032.v
parent3f64bd23a343bcd7be0ef07afa7d9e3249df24ec (diff)
Move opened bugs to bugs/opened
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, 0 insertions, 22 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v
deleted file mode 100644
index 39a7103d1..000000000
--- a/test-suite/bugs/closed/HoTT_coq_032.v
+++ /dev/null
@@ -1,22 +0,0 @@
-(* -*- mode: coq; coq-prog-args: ("-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. *)