Removing a bunch of generic equalities.

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

5 files changed, 8 insertions, 7 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 475bc098a..a0d0cc2ec 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -228,8 +228,8 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
     | Entries.DefinitionEntry ({
       const_entry_opaque = false; const_entry_body = bo } as de) ->
         let pt, seff = Future.force bo in
-        if seff = Declareops.no_seff then cd
-        else begin 
+        if Declareops.side_effects_is_empty seff then cd
+        else begin
           Declareops.iter_side_effects declare_sideff seff;
           Entries.DefinitionEntry { de with
             const_entry_body = Future.from_val (pt, Declareops.no_seff) }
diff --git a/library/goptions.ml b/library/goptions.ml
index 6e2c6ae72..d38d2762a 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -195,7 +195,7 @@ type 'a option_sig = {
 module OptionOrd =
 struct
   type t = option_name
-  let compare = compare
+  let compare opt1 opt2 = List.compare String.compare opt1 opt2
 end
 
 module OptionMap = Map.Make(OptionOrd)
diff --git a/library/lib.ml b/library/lib.ml
index e1dd9ae39..0580661c5 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -513,13 +513,14 @@ let close_section () =
 type frozen = Names.DirPath.t option * library_segment
 
 let freeze ~marshallable =
-  if marshallable = `Shallow then
+  match marshallable with
+  | `Shallow ->
     (* TASSI: we should do something more sensible here *)
     let _, initial_prefix =
       CList.split_when (function _, CompilingLibrary _ -> true | _ -> false)
       !lib_stk in
     !comp_name, initial_prefix
-  else
+  | _ ->
     !comp_name, !lib_stk
 
 let unfreeze (mn,stk) =
diff --git a/library/library.ml b/library/library.ml
index 2a495f0cf..a15b66d20 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -339,7 +339,7 @@ module OpaqueTables = struct
  let store c =
   let n = !local_index in
   incr local_index;
-  if n = Array.length !local_table then begin
+  if Int.equal n (Array.length !local_table) then begin
     let t = Array.make (2*n) a_constr in
     Array.blit !local_table 0 t 0 n;
     local_table := t
diff --git a/library/summary.ml b/library/summary.ml
index d1bbf7191..af4deb40f 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -71,7 +71,7 @@ let unfreeze_summaries fs =
   with Not_found -> anomaly (str"Undeclared summary "++str ml_modules_summary));
   Hashtbl.iter
     (fun id decl ->
-       if id = ml_modules_summary then () (* already unfreezed *)
+       if String.equal id ml_modules_summary then () (* already unfreezed *)
        else
          try decl.unfreeze_function (String.Map.find id fs)
          with Not_found -> decl.init_function())