diff options
| author | bertot | 2006-08-08 14:39:48 +0000 |
|---|---|---|
| committer | bertot | 2006-08-08 14:39:48 +0000 |
| commit | 41e4d9cb0757f8057c0815fa0679e888e57ab604 (patch) | |
| tree | 4f6a7c5aaf8f75dfb46e1077b919b67bd97d1554 | |
| parent | 7e13b8a0627c09a49487dc64210fa4616cffc66c (diff) | |
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
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 7977d4e0f6..5654af0b35 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -1450,7 +1450,7 @@ let prove_principle_for_gen let wf_tac = if is_mes then - Recdef.tclUSER_if_not_mes + (fun b -> Recdef.tclUSER_if_not_mes b None) else fun _ -> prove_with_tcc tcc_lemma_ref [] in let start_tac g = diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index ed2e5b5f50..d6b0d658c9 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -574,11 +574,11 @@ let hyp_terminates func = -let tclUSER_if_not_mes is_mes = +let tclUSER_if_not_mes is_mes names_to_suppress = if is_mes then tclCOMPLETE (h_apply (delayed_force well_founded_ltof,Rawterm.NoBindings)) - else tclUSER is_mes None + else tclUSER is_mes names_to_suppress let start is_mes input_type ids args_id relation rec_arg_num rec_arg_id tac wf_tac : tactic = begin @@ -631,7 +631,7 @@ let start is_mes input_type ids args_id relation rec_arg_num rec_arg_id tac wf_t ) [ (* interactive proof of the well_foundness of the relation *) - wf_tac is_mes; + wf_tac is_mes (Some args_id); (* well_foundness -> Acc for any element *) observe_tac "apply wf_thm" |