More monomorphizations

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

4 files changed, 24 insertions, 11 deletions

diff --git a/lib/cArray.ml b/lib/cArray.ml
index 4615ad0388..a5e38534f3 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -102,7 +102,9 @@ let compare item_cmp v1 v2 =
     cmp (Array.length v1 - 1)
 
 let equal cmp t1 t2 =
-  Array.length t1 = Array.length t2 &&
+  if t1 == t2 then true else
+  if not (Array.length t1 = Array.length t2) then false
+  else
   let rec aux i =
     (i = Array.length t1) || (cmp t1.(i) t2.(i) && aux (i + 1))
   in aux 0
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 130bbcf2fe..5568813329 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -36,7 +36,7 @@ let rec lift_rtree_rec depth n = function
   | Rec(j,defs) ->
       Rec(j, Array.map (lift_rtree_rec (depth+1) n) defs)
 
-let lift n t = if n=0 then t else lift_rtree_rec 0 n t
+let lift n t = if Int.equal n 0 then t else lift_rtree_rec 0 n t
 
 (* The usual subst operation *)
 let rec subst_rtree_rec depth sub = function
@@ -153,12 +153,21 @@ let compare_rtree f = fold2
     if b < 0 then false
     else if b > 0 then true
     else match expand t1, expand t2 with
-        Node(_,v1), Node(_,v2) when Array.length v1 = Array.length v2 ->
+        Node(_,v1), Node(_,v2) when Int.equal (Array.length v1) (Array.length v2) ->
           Array.for_all2 cmp v1 v2
       | _ -> false)
 
+let rec raw_eq cmp t1 t2 = match t1, t2 with
+| Param (i1, j1), Param (i2, j2) ->
+  Int.equal i1 i2 && Int.equal j1 j2
+| Node (x1, a1), Node (x2, a2) ->
+  cmp x1 x2 && Array.equal (raw_eq cmp) a1 a2
+| Rec (i1, a1), Rec (i2, a2) ->
+  Int.equal i1 i2 && Array.equal (raw_eq cmp) a1 a2
+| _ -> false
+
 let eq_rtree cmp t1 t2 =
-  t1 == t2 || t1=t2 ||
+  t1 == t2 || raw_eq cmp t1 t2 ||
   compare_rtree
     (fun t1 t2 ->
       if cmp (fst(dest_node t1)) (fst(dest_node t2)) then 0
@@ -175,8 +184,8 @@ let rec pp_tree prl t =
         hov 2 (str"("++prl lab++str","++brk(1,0)++
                prvect_with_sep pr_comma (pp_tree prl) v++str")")
     | Rec(i,v) ->
-        if Array.length v = 0 then str"Rec{}"
-        else if Array.length v = 1 then
+        if Int.equal (Array.length v) 0 then str"Rec{}"
+        else if Int.equal (Array.length v) 1 then
           hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}")
         else
           hov 2 (str"Rec{"++int i++str","++brk(1,0)++
diff --git a/lib/system.ml b/lib/system.ml
index 84706d0313..a2b371b1fc 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -24,7 +24,7 @@ let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
 
 let ok_dirname f =
   f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) &&
-  (Unicode.ident_refutation f = None)
+  (match Unicode.ident_refutation f with None -> true | _ -> false)
 
 let all_subdirs ~unix_path:root =
   let l = ref [] in
@@ -37,11 +37,13 @@ let all_subdirs ~unix_path:root =
 	if ok_dirname f then
 	  let file = Filename.concat dir f in
 	  try
-	    if (stat file).st_kind = S_DIR then begin
-	      let newrel = rel@[f] in
+            begin match (stat file).st_kind with
+	    | S_DIR ->
+	      let newrel = rel @ [f] in
 	      add file newrel;
 	      traverse file newrel
-	    end
+            | _ -> ()
+            end
 	  with Unix_error (e,s1,s2) -> ()
       done
     with End_of_file ->
diff --git a/lib/util.ml b/lib/util.ml
index fcbd969ab5..8d8c947c74 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -29,7 +29,7 @@ let pi3 (_,_,a) = a
 let is_letter c = (c >= 'a' && c <= 'z') or (c >= 'A' && c <= 'Z')
 let is_digit c = (c >= '0' && c <= '9')
 let is_ident_tail c =
-  is_letter c or is_digit c or c = '\'' or c = '_'
+  is_letter c or is_digit c || c = '\'' or c = '_'
 let is_blank = function
   | ' ' | '\r' | '\t' | '\n' -> true
   | _ -> false