The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

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).