The Coq mailing list

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

Thanks, Pierre & Jason --

Pierre, I think you are right, [vm_cast_no_check] is something like what I need. I have been using [exact_no_check] which is what is called by [vm_cast_no_check]. This took a little bit of reverse engineering, but I finally figured out the problem. There seems to still be a syntactic check for unification variables that is done regardless of whether you use [exact_no_check] or [vm_cast_no_check] but if you let bind the unification variables you can get around it. There are a few more details in the plugin that I wrote to expose this.

https://github.com/gmalecha/coq-checkless/blob/master/test-suite/example.v

Thanks again for your help.

On Thu, Aug 15, 2013 at 3:47 AM, Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr> wrote:

Hi,

I would say that the secret tactic "vm_cast_no_check" is what you are looking for but I don't really know its behavior and … there is no mention of it in any documentation ...

I only know that it is what proofs-by-reflexion-gourrou need in order to compute stuff only one time.

All the best,

Pierre B.

Le 15 août 2013 à 04:26, Jason Gross <jasongross9 AT gmail.com> a écrit :

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/

--

gregory malecha

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