diff options
| -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" |