The Coq mailing list

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

Dear Christian,

A couple years back I started writing a Howto on ML level customization.
It is now available on

http://coq.inria.fr/cocorico/CoqCustomizationHowTo

It is very incomplete and may be somewhat out of date but may provide 
some help.

For your concrete problem I think you need to add some TACTIC EXTEND 
incantation to some .ml4 file  (grep for it in the original .ml4 files).

Hope this helps,

Pierre


Christian Doczkal a écrit :
> Hello again
>
> > [...] Good luck,
> > Sean
>
> Thanks ;)
>
> I'm still trying to understand how to extend Coq with user defined
> tactics. 
>
> I now have a (renamed) copy of the Coq standard tactic "absurd" and get
> it compiled to some absurd.cmx file. I can even build a new toplevel
> using
>
> coqmktop -opt -o mytop.out absurd.cmx
>
> But if I try to call "my_absurd" I get:
>
> Error: The reference my_absurd was not found in the current environment.
>
> So what else do I have to do, to actually be able to call the linked in
> tactic? I have renamed the function "absurd" in the .mi as well as in
> the .mli file.

--
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

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature