In the old version, recursive functions cannot be declared inside a section

when the termination argument is based on the fact that some relation is
well-founded.  The goal correspond to the proof that the relation is
well-founded is cleared of all useless hypotheses and variables, including
variables that maybe used in the intermediary lemma that gathers all the
proofs that need to be done interactively.  As a result, this intermediary
lemma cannot be re-used to prove this goal.  The message is:
Error: No such section variable or assumption : A

This message appears at the time the user send the Qed command.
This is problem report #PR1202 submitted by X. Leroy.

The correction is to use the list of input variables to the function as
the list of variables that should be cleared from the context.
The function tclUSER_if_not_mes needs to be modified.  This function
is also used in contrib/funind/functional_principles_proofs.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9064 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions