The Coq mailing list

[Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>]

Hi,

This was our rationale to create otags, a fews year ago (joined work
with Cuithlauac Alvarado, who had the same problem).  Otags in now
maintained by Hendrik Tews and packaged in linux distros (Debian
Ubuntu at least).

Of course it is far from a semantic answer.

Hope this may help anyway.

  JF

On Fri, Oct 24, 2008 at 06:24:41PM +0800, Razvan Voicu wrote:
> 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
>  

-- 
Jean-Francois Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46