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/extraction/table.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/extraction/table.ml')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a541211391..74728f4124 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -175,7 +175,7 @@ let add_recursors env kn =
     make_con_equiv
       (modpath (user_mind kn))
       (modpath (canonical_mind kn))
-      Dir_path.empty (label_of_id id)
+      Dir_path.empty (Label.of_id id)
   in
   let mib = Environ.lookup_mind kn env in
   Array.iter
@@ -245,8 +245,8 @@ let safe_basename_of_global r =
       anomaly "Inductive object unknown to extraction and not globally visible"
   in
   match r with
-    | ConstRef kn -> id_of_label (con_label kn)
-    | IndRef (kn,0) -> id_of_label (mind_label kn)
+    | ConstRef kn -> Label.to_id (con_label kn)
+    | IndRef (kn,0) -> Label.to_id (mind_label kn)
     | IndRef (kn,i) ->
       (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename
        with Not_found -> last_chance r)
@@ -268,7 +268,7 @@ let safe_pr_long_global r =
   with _ -> match r with
     | ConstRef kn ->
 	let mp,_,l = repr_con kn in
-	str ((string_of_mp mp)^"."^(string_of_label l))
+	str ((string_of_mp mp)^"."^(Label.to_string l))
     | _ -> assert false
 
 let pr_long_mp mp =
-- 
cgit v1.2.3