The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

> --__--__--
> 
> Message: 1
> Date: Thu, 09 Oct 2003 16:36:51 -0400
> From: Nadeem Abdul Hamid 
> <nadeem AT acm.org>
> Organization: Yale University
> To: 
> coq-club AT pauillac.inria.fr
> Subject: [Coq-Club] OCaml tactics
> 
> Hi,
> 
> 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.
> 
> which applies to a hypothesis of form:
> 
> H: (EX m:nat | P(m))
> 
> < ElimEx H m.
> 
> would result in:
> 
> m: nat
> H: P(m)
> 
> Now, instead of doing this in the toplevel tactic language of Coq, how 
> could you write the same tactic in OCaml and what tools do you use to 
> load it into the toplevel.
> 
> Thanks for your help,
> 
> --- nadeem
> 

I wrote a few tactics at the Ocaml level, and every time, I did it by
copying and pasting from other examples.  The examples to get
inspiration from are in the contrib/ directory rather than the tactics 
directory.

Perhaps an even better solution is to use examples from the users'
contributions.  From a quick check, I gather that the contributions

   cps.tar.gz expceptions.tar.gz fta.tar.gz rational-numbers.tar.gz

(especially the last two) should contain tactics written in ml

Other contributions also contain ml code, but I think that ml code is
extracted from proofs, they do not correspond to tactics.

I hope this helps,

  Yves


PS. To find the contributions that contain ml code, I used the
following command (I use bash).

for i in *.tar.gz ; do tar tfz $i | grep '\.ml' > /tmp/bertot-bidon; if [ -s 
/tmp/bertot-bidon ] ; then echo $i ; cat /tmp/bertot-bidon ; fi ; done | less