The Coq mailing list

[Pierre Corbineau <Pierre.Corbineau AT imag.fr>]

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/
begin:vcard
fn:Pierre Corbineau
n:Corbineau;Pierre
org;quoted-printable:Universit=C3=A9 Joseph Fourier - Grenoble 1;Laboratoire VERIMAG - Polytech' Grenoble
adr;quoted-printable;quoted-printable:2, avenue de Vignate;;VERIMAG - Centre =C3=89QUATION ;GI=C3=88RES ;;38610;France
email;internet:Pierre.Corbineau AT imag.fr
title;quoted-printable:Ma=C3=AEtre de Conf=C3=A9rences
tel;work:+33 (0) 4 56 52 04 42
tel;fax:+33 (0) 4 56 52 03 44
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~corbinea
version:2.1
end:vcard