coq
coq copied to clipboard
Anomaly: Mismatched instance and context when building universe substitution. on coqc -xml
If bug05.v is
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'
}.
I get
$ coqc -xml -debug -q -I . bug05
File "./bug05.v", line 13, characters 0-187:
Anomaly: Mismatched instance and context when building universe substitution.
Please report.
frame @ file "toplevel/vernac.ml", line 420, characters 12-38
raise @ file "toplevel/vernac.ml", line 111, characters 8-56
frame @ file "toplevel/vernac.ml", line 374, characters 27-64
frame @ file "toplevel/vernac.ml", line 348, characters 11-32
frame @ file "toplevel/vernac.ml", line 343, characters 6-16
raise @ file "toplevel/vernac.ml", line 335, characters 18-25
frame @ file "toplevel/vernac.ml", line 327, characters 14-104
raise @ file "library/states.ml", line 40, characters 45-46
frame @ file "library/states.ml", line 38, characters 4-7
raise @ file "lib/flags.ml", line 15, characters 10-17
frame @ file "lib/flags.ml", line 11, characters 14-17
raise @ file "toplevel/vernacentries.ml", line 1829, characters 12-13
frame @ file "toplevel/vernacentries.ml", line 1818, characters 4-12
frame @ file "toplevel/vernacentries.ml", line 546, characters 10-90
frame @ file "toplevel/record.ml", line 470, characters 11-178
frame @ file "toplevel/record.ml", line 332, characters 11-97
frame @ file "toplevel/command.ml", line 504, characters 15-40
frame @ file "library/declare.ml", line 321, characters 2-41
frame @ file "plugins/xml/xmlcommand.ml", line 403, characters 32-91
frame @ file "plugins/xml/xmlcommand.ml", line 241, characters 4-663
frame @ file "array.ml", line 128, characters 9-30
frame @ file "kernel/inductive.ml", line 178, characters 6-38
frame @ file "kernel/inductive.ml", line 56, characters 4-44
raise @ file "lib/errors.ml", line 27, characters 18-39