The Coq mailing list

[Jan-Oliver Kaiser <janno AT mpi-sws.org>]

Hi,

I've been trying to perform a seemingly trivial feet but I am not 
getting anywhere with it. My eventual goal is to define multiple 
constants, some of which contain proofs which I can only construct by 
evaluating previously defined constants. This is supposed to happen in 
one vernacular command.

In my current setup I am trying to mirror what happens in the Definition 
vernacular, i.e. calling Command.declare_definition. Once the vernacular 
command is fully interpreted the definition is ready to be used, 
evaluated, etc. So far so good. However, within the command (after 
calling declare_definition) I seem to be unable to delta-reduce the 
constant. My attempts fail with "Uncaught Exception Not_found" in hMap.ml.

Now, seeing how the constant is eventually declared correctly at the end 
of the command, I wonder what it is I need to do within the command to 
achieve the same effect earlier.

Any help is much appreciated!

Cheers
Jan-Oliver