The Coq mailing list

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

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 ?

thanks,
Julien