The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I do not know much about vm_cast, nor Coq source, but I know that appcontext can be used to delay type-checking, such as in

Goal 1 = 2.                                                                      

  match goal with                                                                

    | [ |- appcontext G[1] ] => let G' := context G[Type] in                     

                                let G'' := constr:(G' = G') in                   

                                pose G''                                            

  end.

(which succeeds, for me).  I seem to recall having some cases where it only works if you use [idtac] (and don't let the ill-typed term escape), but I can't find them.  (I think of [appcontext] and [context] as the sledge-hammer to smash through Coq's type-checked syntax tree.

I hope this helps.

-Jason

On Wednesday, August 14, 2013, Gregory Malecha wrote:

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/