The Coq mailing list

[Cuihtlauac ALVARADO <cuihtlauac.alvarado AT rd.francetelecom.com>]

Hi Nadeem,

Writing ML tactics seems a bit old fashioned today :-( Fortunately, I
like vintage stuff :-)

On Thu, Oct 09, 2003 at 04:36:51PM -0400, Nadeem Abdul Hamid wrote:
> 
> How does one go about writing tactics for Coq at the OCaml level?
> I've looked through the /tactics directory in the source
> distribution but don't know really where to get started.
> 
> Maybe a complete example would be helpful. For example, take the
> simple tactic below:
>
> < Tactic Definition ElimEx hyp var := Elim hyp; Clear hyp; Intros var hyp.

Basically, this Ocaml code will do the job:

let (>>) = Tacticals.tclTHEN

let tac_in_concl =
    Tactics.intro
 >> (Tacticals.tclLAST_HYP Tactics.simplest_elim)
 >> (Tacticals.tclLAST_HYP (fun x -> Tactics.clear [Term.destVar x]))

The nice point is tclLAST_HYP which permits writing the tactic without
introducing any fresh name. Writing Makefile and .ml4 file is simple
but somehow counter-intuitive. Like Yves said, dig the contrib to find
examples. You'll find mine in this archive file :

  http://perso.rd.francetelecom.fr/alvarado/soft/nadeem-0.1.tgz

I've also made available another simple example called "Convert". This
tactics make something in between Change and Unfold, but in a Rewrite
style.

  http://perso.rd.francetelecom.fr/alvarado/soft/convert-0.1.tgz

Hope it helps

-- 
Cuihtlauac ALVARADO - France Telecom R&D - DTL/TAL
2, avenue Pierre Marzin - 22307 Lannion - France
Tel: +33 2 96 05 32 73 - Fax: +33 2 96 05 39 45