From aa37087b8e7151ea96321a11012c1064210ef4ea Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 18 Dec 2012 17:09:31 +0000
Subject: Modulification of Label

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/functional_principles_proofs.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

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*)
-- 
cgit v1.2.3