Monomorphization (lib)

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

5 files changed, 34 insertions, 15 deletions

diff --git a/lib/cList.ml b/lib/cList.ml
index debfa09be..78c17c3ff 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -56,6 +56,7 @@ sig
   include S
   val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
   val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
+  val is_empty : 'a list -> bool
   val add_set : 'a -> 'a list -> 'a list
   val eq_set : 'a list -> 'a list -> bool
   val intersect : 'a list -> 'a list -> 'a list
@@ -334,6 +335,10 @@ let rec equal cmp l1 l2 =
       cmp x1 x2 && equal cmp l1 l2
     | _ -> false
 
+let is_empty = function
+| [] -> true
+| _ -> false
+
 let intersect l1 l2 =
   filter (fun x -> List.mem x l2) l1
 
diff --git a/lib/cList.mli b/lib/cList.mli
index 2e0d519a1..9b3a988ab 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -63,6 +63,9 @@ sig
   val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool
   (** Lifts equality to list type. *)
 
+  val is_empty : 'a list -> bool
+  (** Checks whether a list is empty *)
+
   val add_set : 'a -> 'a list -> 'a list
   (** [add_set x l] adds [x] in [l] if it is not already there, or returns [l]
       otherwise. *)
diff --git a/lib/option.ml b/lib/option.ml
index 2c7bb6111..9ed0bda87 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -19,6 +19,10 @@ let has_some = function
   | None -> false
   | _ -> true
 
+let is_empty = function
+| None -> true
+| Some _ -> false
+
 exception IsNone
 
 (** [get x] returns [y] where [x] is [Some y]. It raises IsNone
diff --git a/lib/option.mli b/lib/option.mli
index 69564ae4d..faae301ab 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -17,6 +17,9 @@
     otherwise.  *)
 val has_some : 'a option -> bool
 
+(** Negation of [has_some] *)
+val is_empty : 'a option -> bool
+
 exception IsNone
 
 (** [get x] returns [y] where [x] is [Some y]. It raises IsNone
diff --git a/lib/system.ml b/lib/system.ml
index a2b371b1f..dbab923af 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -23,7 +23,8 @@ let skipped_dirnames = ref ["CVS"; "_darcs"]
 let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
 
 let ok_dirname f =
-  f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) &&
+  not (String.equal f "") && f.[0] != '.' &&
+  not (List.mem f !skipped_dirnames) &&
   (match Unicode.ident_refutation f with None -> true | _ -> false)
 
 let all_subdirs ~unix_path:root =
@@ -60,19 +61,22 @@ let where_in_path ?(warn=true) path filename =
 	  then (lpe,f) :: search rem
 	  else search rem
     | [] -> [] in
-  let check_and_warn l =
-    match l with
-      | [] -> raise Not_found
-      | (lpe, f) :: l' ->
-	  if warn & l' <> [] then
-	    msg_warning
-	      (str filename ++ str " has been found in" ++ spc () ++
-	       hov 0 (str "[ " ++
-	         hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
-		   (fun (lpe,_) -> str lpe) l)
-	         ++ str " ];") ++ fnl () ++
-	       str "loading " ++ str f);
-	  (lpe, f) in
+  let check_and_warn l = match l with
+  | [] -> raise Not_found
+  | (lpe, f) :: l' ->
+    let () = match l' with
+    | _ :: _ when warn ->
+      msg_warning
+        (str filename ++ str " has been found in" ++ spc () ++
+          hov 0 (str "[ " ++
+            hv 0 (prlist_with_sep (fun () -> str " " ++ pr_semicolon())
+              (fun (lpe,_) -> str lpe) l)
+            ++ str " ];") ++ fnl () ++
+          str "loading " ++ str f)
+    | _ -> ()
+    in
+    (lpe, f)
+  in
   check_and_warn (search path)
 
 let find_file_in_path ?(warn=true) paths filename =
@@ -123,7 +127,7 @@ let raw_extern_intern magic suffix =
     filename,channel
   and intern_state filename =
     let channel = open_in_bin filename in
-    if input_binary_int channel <> magic then
+    if not (Int.equal (input_binary_int channel) magic) then
       raise (Bad_magic_number filename);
     channel
   in