diff options
| author | ppedrot | 2012-12-18 17:09:31 +0000 |
|---|---|---|
| committer | ppedrot | 2012-12-18 17:09:31 +0000 |
| commit | aa37087b8e7151ea96321a11012c1064210ef4ea (patch) | |
| tree | fff9ed837668746545832e3bd9f0a6dd99936ee4 /plugins/funind/functional_principles_proofs.ml | |
| parent | f61e682857596f0274b956295efd2bfba63bc8c0 (diff) | |
Modulification of Label
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index ca73799c18..9c895e6a9c 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -966,7 +966,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in - let f_id = id_of_label (con_label (destConst f)) in + let f_id = Label.to_id (con_label (destConst f)) in let prove_replacement = tclTHENSEQ [ @@ -1000,7 +1000,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g = let finfos = find_Function_infos (destConst f) in mkConst (Option.get finfos.equation_lemma) with (Not_found | Option.IsNone as e) -> - let f_id = id_of_label (con_label (destConst f)) in + let f_id = Label.to_id (con_label (destConst f)) in (*i The next call to mk_equation_id is valid since we will construct the lemma Ensures by: obvious i*) |