DanGrayson/coq

Prop problem

Closed this issue · 1 comments

DanGrayson commented

The patched version of coq 8.3 rejected this:

   Definition this_works : (nat = nat : Set) = (nat = nat : Prop) := eq_refl.

and so should this version of coq.

See the change to evd.ml in commit f23efe4

DanGrayson commented

It's not actually an issue, because we don't use "=" as the identity type.