The Coq mailing list

[Julien Tesson <julien.tesson AT univ-orleans.fr>]

Le 11/05/2011 11:44, Julien Tesson a écrit :
> Hi,
> I am trying to use Ltac and context to do something like
>
> Ltac f x := 
>    match x with
>      context f [ SomeTermIwantToReplace ] => let x':=fun p => context f[ 
> a_replacement_function p]
>        in assert (forall p, (x' p))
>    end.
>
> but this syntax dos not work and I was unable to find a way to do it.
>
> After a discussion on the IRC channel I try miscellaneous attempt : 
> http://pastebin.com/aJ3vQ1kz ;.
>
> Here I really need to have, after I prove the assertion, an hypothesis like 
> this [forall p , x' p],
> so I cannot first introduce  p to the environment  and then apply the 
> replacement tactic.
>
> As someone any idea on how to proceed ?
The reason seems to be that  "context f[ a_replacement_function p]" as to be 
a type checkable term, is it true ?
Is it a desired feature, or just a technical constraint in  the Ltac 
implementation ?

Actually, it would be sometimes very practical to generate  a  kind of 
preterm with a tactic, and to be able to pass it to other tactics.

-- 
Julien Tesson

Doctorant - ATER
Laboratoire d'Informatique Fondamentale d'Orléans
Département Informatique
Université d'Orléans

Tel : 02 38 49 25 81
Fax : 09 56 45 86 27
http://tesson.julien.free.fr/