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.
Here is some code that works in 8.4pl3 and HoTT/coq, but fails in trunk-polyproj
(* File reduced by coq-bug-finder from original input, then from 3329 lines to 153 lines, then from 118 lines to 49 lines, then from \
55 lines to 38 lines, then from 46 lines to 16 lines *)
Generalizable All Variables.
Set Universe Polymorphism.
Class Foo (A : Type) := {}.
Definition Bar {A B} `{Foo A, Foo B} : True.
Proof.
Set Printing Universes.
change Foo with Foo in *.
admit.
Defined.
Definition foo := @Bar nat.
Check @foo Set.
(* Toplevel input, characters 26-29:
Error:
The term "Set" has type "Type (* Set+1 *)" while it is expected to have type
"Set" (Universe inconsistency: Cannot enforce Set < Set because Set = Set)). *)
Here is some code that works in 8.4pl3 and HoTT/coq, but fails in trunk-polyproj
I believe this is the same bug as #107.