The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

Hello --

I want to construct a term like this:

exact (@eq_refl T Z <: Y = Z)

but the term Y contains unification variables so the vm_cast will fail. Is there any way for me to build this term without having the type checker check it until the [Qed]? I realize that this would mean that if there was an error it would not be caught until the [Qed] but I'm fine with that.

I realize that you can't do this in Ltac so I was digging through the Coq source and found [exact_no_check] which I thought would work, and looks like it should (I can't find the place where it is performing any sort of checking on the term), but for some reason it is still failing. Does anyone have any pointers or suggestions for how to get this to work?

Thank you.

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/