The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

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