search

HoTT / coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
http://coq.inria.fr/
GNU Lesser General Public License v2.1
27 stars 5 forks source link

Anomaly: File "toplevel/himsg.ml": Assertion failed. Please report. #94

Closed JasonGross closed 10 years ago

JasonGross commented 10 years ago

This doesn't seem to happen in polyproj, only in HoTT/coq trunk.

Record PreCategory :=  Build_PreCategory' { object :> Type }.
Class Foo (X : Type) := {}.
Class Bar := {}.
Definition functor_category `{Bar} (C D : PreCategory)  `{Foo (object D)} : PreCategory.
Admitted.
Definition functor_object_of `{Bar} (C1 C2 D : PreCategory) `{Foo (object D)}
: functor_category C1 (functor_category C2 D) -> True.
(** Anomaly: File "toplevel/himsg.ml", line ..., characters ...: Assertion failed.
Please report. *)
JasonGross commented 10 years ago

This seems to be fixed in the most recent version of trunk-polyproj.