The Coq mailing list

[St�phane Glondu <steph AT glondu.net>]

Le 06/03/2012 10:31, Francois Pottier a écrit :
>> Did you come up with a pure Ltac solution?
> 
> Yes, I used your previous suggestion, "unfold f; fold f", which happens to
> work for me. Prior to that I use "match goal with ... ?f ..." to gain access
> to the name "f".

Well... "unfold f; fold f" is just an approximation of what you asked.

>> This precisely can be done easily with a plugin in OCaml.
> 
> Very interesting, thanks. Is there documentation somewhere on how to write
> plugins?

Not really. I would learn by looking at other plugins and Coq's source
code, and by asking around. I've written the following page a while ago:

  http://coq.inria.fr/cocorico/evar_match

I've just created:

  http://coq.inria.fr/cocorico/UnfoldFixpointOnce

In my opinion, tactics written in OCaml are often more reliable (you can
program exactly what you want, whereas tactics exposed to Ltac are
usually very high level) than a composition of approximations written in
Ltac. Moreover, I believe it's not significantly more difficult to port
a (non-trivial yet simple) plugin to a new version of Coq, compared to a
regular, pure Gallina (but complex), development.


Cheers,

-- 
Stéphane