The Coq mailing list

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

Sorry for this double post. 

I thought (monday) my first mail (friday) had some trouble.

On Mon, Oct 13, 2003 at 10:38:13AM +0200, Cuihtlauac ALVARADO wrote:
> 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
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
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