The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> Back in coq v6, there is a chapter in the reference manual to tell you 
> how to write coq tactics in ocaml (Part III User extensions, Chapter 10 
> Writing ad-hoc Tactics in Coq), but I cannot find similar information 
> from the latest reference manual for coq v8.
 
> Is such information available for coq v8? 

  It has to be done but unfortunately it is not.

> If not, can I still use the material from the v6 reference manual as
> a starting point?

  Coq data structures and Ocaml entry points in the source of Coq have
really changed a lot since V6. You'll have to study the source
(typically the files kernel/term.ml, pretyping/termops.ml,
tactics/tactics.ml, tactics/tacticals.ml, tactics/extratactics.ml4,
... see also the files in dev).

  You may also find help on this list.

  Hugo Herbelin