From aa37087b8e7151ea96321a11012c1064210ef4ea Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
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/xml/cic2acic.ml            | 6 +++---
 plugins/xml/doubleTypeInference.ml | 2 +-
 plugins/xml/xmlcommand.ml          | 6 +++---
 3 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'plugins/xml')

diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index fb951b35f..4a8436d76 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -128,12 +128,12 @@ let token_list_of_kernel_name tag =
  let module GN = Globnames in
  let id,dir = match tag with
    | Variable kn ->
-       N.id_of_label (N.label kn), Lib.cwd ()
+       N.Label.to_id (N.label kn), Lib.cwd ()
    | Constant con ->
-       N.id_of_label (N.con_label con),
+       N.Label.to_id (N.con_label con),
        Lib.remove_section_part (GN.ConstRef con)
    | Inductive kn ->
-       N.id_of_label (N.mind_label kn),
+       N.Label.to_id (N.mind_label kn),
        Lib.remove_section_part (GN.IndRef (kn,0))
  in
  token_list_of_path dir id (etag_of_tag tag)
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index b4ec85ab7..864f35e80 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -21,7 +21,7 @@ let cprop =
    (N.MPfile
      (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
    (N.Dir_path.make [])
-   (N.mk_label "CProp")
+   (N.Label.make "CProp")
 ;;
 
 let whd_betadeltaiotacprop env _evar_map ty =
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 50309317e..e16f9dd19 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -384,12 +384,12 @@ let print internal glob_ref kind xml_library_root =
        (* this kn is fake since it is not provided by Coq *)
        let kn =
         let (mod_path,dir_path) = Lib.current_prefix () in
-        N.make_kn mod_path dir_path (N.label_of_id id)
+        N.make_kn mod_path dir_path (N.Label.of_id id)
        in
        let (_,body,typ) = G.lookup_named id in
         Cic2acic.Variable kn,mk_variable_obj id body typ
     | Gn.ConstRef kn ->
-       let id = N.id_of_label (N.con_label kn) in
+       let id = N.Label.to_id (N.con_label kn) in
        let cb = G.lookup_constant kn in
        let val0 = D.body_of_constant cb in
        let typ = cb.D.const_type in
@@ -467,7 +467,7 @@ let _ =
          (* I saved in the Pfedit.set_xml_cook_proof callback.          *)
         let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in
          show_pftreestate internal fn pftreestate
-	  (Names.id_of_label (Names.con_label kn)) ;
+	  (Names.Label.to_id (Names.con_label kn)) ;
          proof_to_export := None)
 ;;
 
-- 
cgit v1.2.3