The Coq mailing list

[Christian Doczkal <doczkal AT ps.uni-sb.de>]

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.

-- 
Regards
Christian