diff options
| author | herbelin | 2009-03-14 21:29:19 +0000 |
|---|---|---|
| committer | herbelin | 2009-03-14 21:29:19 +0000 |
| commit | 208f162ab68d00488248ee052947592dd23d5d52 (patch) | |
| tree | 4009b4e1da390933e5ccfc878390478041c6679a /contrib/funind/functional_principles_proofs.ml | |
| parent | 4b7200cbbf4f2462d6f1398a191377b4d57f7655 (diff) | |
Cleaning/uniformizing the interface of tacticals.mli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11980 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind/functional_principles_proofs.ml')
| -rw-r--r-- | contrib/funind/functional_principles_proofs.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml index 75b811d518..adfb9ce2ff 100644 --- a/contrib/funind/functional_principles_proofs.ml +++ b/contrib/funind/functional_principles_proofs.ml @@ -1015,7 +1015,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = (tclDO nb_intro_to_do intro) ( fun g' -> - let just_introduced = nLastHyps nb_intro_to_do g' in + let just_introduced = nLastDecls nb_intro_to_do g' in let just_introduced_id = List.map (fun (id,_,_) -> id) just_introduced in tclTHEN (Equality.rewriteLR equation_lemma) (revert just_introduced_id) g' ) @@ -1218,7 +1218,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : [ (* observe_tac ("introducing args") *) (tclDO nb_args intro); (fun g -> (* replacement of the function by its body *) - let args = nLastHyps nb_args g in + let args = nLastDecls nb_args g in let fix_body = fix_info.body_with_param in (* observe (str "fix_body := "++ pr_lconstr_env (pf_env gl) fix_body); *) let args_id = List.map (fun (id,_,_) -> id) args in @@ -1282,7 +1282,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams : [ tclDO nb_args intro; (fun g -> (* replacement of the function by its body *) - let args = nLastHyps nb_args g in + let args = nLastDecls nb_args g in let args_id = List.map (fun (id,_,_) -> id) args in let dyn_infos = { |