The Coq mailing list

[Julien Tesson <julien.tesson AT lacl.fr>]

Hi all !
I am currently trying to make some tactics that return values, to be used by 
other tactics, but I have some trouble to mix this "functional style" with 
the usual "imperative style".
I'd like to write tactics that first do some operations on the environment 
and then return a term like this one :

Ltac test_return :=
 let H := True in
  assert (H=True) by reflexivity;
  constr:H.

Coq lets me define such Ltac function, but then, when I try to use it, like 
this :

Ltac  mem mem_arg :=
      let H := fresh "Mem" in
      pose (H := mem_arg)
    .

mem ltac:(test_return).  

I get the error : "Variable mem_arg should be bound to a term". It makes me 
think that no value is returned by the tactic called.

The only workaround I found was to use a "continuation passing style" like 
this :

Ltac test_cont  cont :=
 let H := True in
  assert (H=True) by reflexivity;
  cont constr:H.

test_return mem.

But I find this style less convenient to use.

So here are my questions :
Is there something that can make test_return work as I expected ?
If not, I'm curious to know why such kind of thing is not permitted ?

-- Julien