The Coq mailing list

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

Dear Jean-Francois,

Thanks for your pointer. It would certainly help with moving faster through
the code-base.

Regards,

Razvan

-----Original Message-----
From: 
coq-club-admin AT pauillac.inria.fr
[mailto:coq-club-admin AT pauillac.inria.fr]
 On Behalf Of Jean-Francois Monin
Sent: Friday, October 24, 2008 8:07 PM
To: Razvan Voicu
Cc: 
coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Guide to Coq Sources

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

--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club