From 67f5c70a480c95cfb819fc68439781b5e5e95794 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 14 Dec 2012 15:56:25 +0000
Subject: Modulification of identifier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/syntax/ascii_syntax.ml   |  6 +++---
 plugins/syntax/numbers_syntax.ml |  4 ++--
 plugins/syntax/r_syntax.ml       |  6 +++---
 plugins/syntax/z_syntax.ml       | 10 +++++-----
 4 files changed, 13 insertions(+), 13 deletions(-)

(limited to 'plugins/syntax')

diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 03fbc7e98..958fdc649 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -16,9 +16,9 @@ open Coqlib
 
 exception Non_closed_ascii
 
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let make_kn dir id = Globnames.encode_mind (make_dir dir) (id_of_string id)
-let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
+let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let ascii_module = ["Coq";"Strings";"Ascii"]
 
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 94d4e0713..f86b56bc7 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -14,8 +14,8 @@ open Glob_term
 
 (*** Constants for locating int31 / bigN / bigZ / bigQ constructors ***)
 
-let make_dir l = Names.make_dirpath (List.map Names.id_of_string (List.rev l))
-let make_path dir id = Libnames.make_path (make_dir dir) (Names.id_of_string id)
+let make_dir l = Names.make_dirpath (List.map Names.Id.of_string (List.rev l))
+let make_path dir id = Libnames.make_path (make_dir dir) (Names.Id.of_string id)
 
 let make_mind mp id = Names.make_mind mp Names.empty_dirpath (Names.mk_label id)
 let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index a40c966fe..f7d0091f3 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -19,14 +19,14 @@ exception Non_closed_number
 open Glob_term
 open Bigint
 
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
+let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
 let rdefinitions = make_dir ["Coq";"Reals";"Rdefinitions"]
-let make_path dir id = Libnames.make_path dir (id_of_string id)
+let make_path dir id = Libnames.make_path dir (Id.of_string id)
 
 let r_path = make_path rdefinitions "R"
 
 (* TODO: temporary hack *)
-let make_path dir id = Globnames.encode_con dir (id_of_string id)
+let make_path dir id = Globnames.encode_con dir (Id.of_string id)
 
 let r_kn = make_path rdefinitions "R"
 let glob_R = ConstRef r_kn
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 8e5a07e0d..9faa6edd1 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -23,15 +23,15 @@ open Glob_term
 
 let binnums = ["Coq";"Numbers";"BinNums"]
 
-let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
-let make_path dir id = Libnames.make_path (make_dir dir) (id_of_string id)
+let make_dir l = make_dirpath (List.map Id.of_string (List.rev l))
+let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
 let positive_path = make_path binnums "positive"
 
 (* TODO: temporary hack *)
 let make_kn dir id = Globnames.encode_mind dir id
 
-let positive_kn = make_kn (make_dir binnums) (id_of_string "positive")
+let positive_kn = make_kn (make_dir binnums) (Id.of_string "positive")
 let glob_positive = IndRef (positive_kn,0)
 let path_of_xI = ((positive_kn,0),1)
 let path_of_xO = ((positive_kn,0),2)
@@ -93,7 +93,7 @@ let _ = Notation.declare_numeral_interpreter "positive_scope"
 (* Parsing N via scopes                                               *)
 (**********************************************************************)
 
-let n_kn = make_kn (make_dir binnums) (id_of_string "N")
+let n_kn = make_kn (make_dir binnums) (Id.of_string "N")
 let glob_n = IndRef (n_kn,0)
 let path_of_N0 = ((n_kn,0),1)
 let path_of_Npos = ((n_kn,0),2)
@@ -144,7 +144,7 @@ let _ = Notation.declare_numeral_interpreter "N_scope"
 (**********************************************************************)
 
 let z_path = make_path binnums "Z"
-let z_kn = make_kn (make_dir binnums) (id_of_string "Z")
+let z_kn = make_kn (make_dir binnums) (Id.of_string "Z")
 let glob_z = IndRef (z_kn,0)
 let path_of_ZERO = ((z_kn,0),1)
 let path_of_POS = ((z_kn,0),2)
-- 
cgit v1.2.3