More monomorphizations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 15 insertions, 10 deletions

diff --git a/library/libnames.ml b/library/libnames.ml
index a07895eec..e51e2c81c 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -50,21 +50,25 @@ let add_dirpath_suffix p id = make_dirpath (id :: repr_dirpath p)
 let parse_dir s =
   let len = String.length s in
   let rec decoupe_dirs dirs n =
-    if n = len && n > 0 then error (s ^ " is an invalid path.");
+    if Int.equal n len && n > 0 then error (s ^ " is an invalid path.");
     if n >= len then dirs else
     let pos =
       try
 	String.index_from s n '.'
       with Not_found -> len
     in
-    if pos = n then error (s ^ " is an invalid path.");
+    if Int.equal pos n then error (s ^ " is an invalid path.");
     let dir = String.sub s n (pos-n) in
     decoupe_dirs ((id_of_string dir)::dirs) (pos+1)
   in
     decoupe_dirs [] 0
 
 let dirpath_of_string s =
-  make_dirpath (if s = "" then [] else parse_dir s)
+  let path = match s with
+  | "" -> []
+  | _ -> parse_dir s
+  in
+  make_dirpath path
 
 let string_of_dirpath = Names.string_of_dirpath
 
@@ -85,8 +89,9 @@ let repr_path { dirpath = pa; basename = id } = (pa,id)
 (* parsing and printing of section paths *)
 let string_of_path sp =
   let (sl,id) = repr_path sp in
-  if repr_dirpath sl = [] then string_of_id id
-  else (string_of_dirpath sl) ^ "." ^ (string_of_id id)
+  match repr_dirpath sl with
+  | [] -> string_of_id id
+  | _ -> (string_of_dirpath sl) ^ "." ^ (string_of_id id)
 
 let sp_ord sp1 sp2 =
   let (p1,id1) = repr_path sp1
diff --git a/library/nameops.ml b/library/nameops.ml
index 5ea7e2685..62665e8af 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -28,16 +28,16 @@ let cut_ident skip_quote s =
   let slen = String.length s in
   (* [n'] is the position of the first non nullary digit *)
   let rec numpart n n' =
-    if n = 0 then
+    if Int.equal n 0 then
       (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *)
       slen
     else
       let c = Char.code (String.get s (n-1)) in
-      if c = code_of_0 && n <> slen then
+      if Int.equal c code_of_0 && n <> slen then
 	numpart (n-1) n'
       else if code_of_0 <= c && c <= code_of_9 then
 	numpart (n-1) (n-1)
-      else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then
+      else if skip_quote && (Int.equal c (Char.code '\'') || Int.equal c (Char.code '_')) then
 	numpart (n-1) (n-1)
       else
 	n'
@@ -48,7 +48,7 @@ let repr_ident s =
   let numstart = cut_ident false s in
   let s = string_of_id s in
   let slen = String.length s in
-  if numstart = slen then
+  if Int.equal numstart slen then
     (s, None)
   else
     (String.sub s 0 numstart,
@@ -75,7 +75,7 @@ let lift_subscript id =
   let rec add carrypos =
     let c = id.[carrypos] in
     if is_digit c then
-      if c = '9' then begin
+      if Int.equal (Char.code c) (Char.code '9') then begin
 	assert (carrypos>0);
 	add (carrypos-1)
       end