The Coq mailing list

["Razvan Voicu" <razvan AT comp.nus.edu.sg>]

Hi,

 

I would like to implement a tactic that performs actions in a manner that is dependent on the shape of the partial proof of the current goal. From what I gather, this can only be done on Ocaml, since LTac makes no provisions for accessing the proof term. So, is there a guide to the Coq source tree? Or, could anyone provide some useful pointers? I would be particularly interested the source files containing the type that implements proof terms and the procedures that manipulate such terms.

 

Thanks in advance,

 

Razvan