The Coq mailing list

[Chung-Kil Hur <gil.hur AT gmail.com>]

Right. It doesn't work.

But in my case I got "Uncaught exception".

I am using Coq 8.4 not 8.4pl1.

 

Anyway, I don't know the reason.

 

By the way, "hget_evar" is what I wrote and put it into Coq from 8.3.

I am not 100% sure whether there is a bug with the code because I am not a real expert.

The code itself is very short (10 lines or so).

It would be nice if some coq expert looks at the code and check whether it is really correct or not because I find the tactic very useful.

 

Best,

Gil

 

On Thu, Jan 24, 2013 at 7:44 PM, Thomas Braibant <thomas.braibant AT gmail.com> wrote:

I tried your tactics on my examples (the one in the github
repository), and I cannot do hide_evars; vm_compute. vm_compute
unfolds the definition that you just put in the hypotheses, using
set...  Could you try and see if I missed something.

In any case, I feel like the repeat hide_evar tactic is sub optimal:
you iterate n times in the goal, with n being the number of
existential variables.

Thomas.
By the way I did not knew this hget_evar tactic, which is
undocumented. It seems nice. For the audience, it folds the nth evar
that appears in the goal as a let.

On Thu, Jan 24, 2013 at 7:24 PM, Chung-Kil Hur <gil.hur AT gmail.com> wrote:
>
> Definition _Evar_Gil_ (A:Type) (x:A) := x.
>
> Tactic Notation "hide_evar" int_or_var(n) := let QQ := fresh "QQ" in
>   hget_evar n; intro;
>   lazymatch goal with [ H := ?X |- _] =>
>     set (QQ := X) in *; fold (@_Evar_Gil_ _ X) in QQ; clear H
>   end.
>
> Ltac hide_evars := repeat (hide_evar 1).
>
> Ltac show_evars :=
>   repeat (match goal with [ H := @_Evar_Gil_ _ _ |- _ ] =>
>     unfold _Evar_Gil_ in H; unfold H in *; clear H end).