The Coq mailing list

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

Dear Pierre,

Thanks for taking the trouble to post the link. However, I'm afraid that the
link does not work. Would you mind checking if there's a typo?

Thanks again,

Razvan

-----Original Message-----
From: 
coq-club-admin AT pauillac.inria.fr
[mailto:coq-club-admin AT pauillac.inria.fr]
 On Behalf Of Pierre Corbineau
Sent: Friday, October 24, 2008 7:47 PM
To: 
razvan AT comp.nus.edu.sg
Cc: 
coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Guide to Coq Sources


Hi,

Some information about internals can be found in

http://logical.futurs.inria.fr/cocorico/CoqCustomizationHowTo

Be careful: this might not be completely up to date information.

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
>  

-- 
Pierre Corbineau          | 
Pierre.Corbineau AT imag.fr
VERIMAG - Centre Équation | Tel: (+33 / 0) 4 56 52 04 42
2, avenue de Vignate      | Office nr B2G2
38610 GIÈRES - FRANCE     | http://www-verimag.imag.fr/~corbinea/