Removing a bunch of generic equalities.

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

1 files changed, 43 insertions, 37 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index dbd280a1e..53bb53606 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -20,7 +20,7 @@ open Mlutil
 let string_of_id id =
   let s = Names.Id.to_string id in
   for i = 0 to String.length s - 2 do
-    if s.[i] = '_' && s.[i+1] = '_' then warning_id s
+    if s.[i] == '_' && s.[i+1] == '_' then warning_id s
   done;
   Unicode.ascii_of_ident s
 
@@ -39,7 +39,7 @@ let pp_apply st par args = match args with
 (** Same as [pp_apply], but with also protection of the head by parenthesis *)
 
 let pp_apply2 st par args =
-  let par' = args <> [] || par in
+  let par' = not (List.is_empty args) || par in
   pp_apply (pp_par par' st) par args
 
 let pr_binding = function
@@ -79,20 +79,20 @@ let is_digit = function
 
 let begins_with_CoqXX s =
   let n = String.length s in
-  n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' &&
+  n >= 4 && s.[0] == 'C' && s.[1] == 'o' && s.[2] == 'q' &&
   let i = ref 3 in
   try while !i < n do
-    if s.[!i] = '_' then i:=n (*Stop*)
+    if s.[!i] == '_' then i:=n (*Stop*)
     else if is_digit s.[!i] then incr i
     else raise Not_found
   done; true
   with Not_found -> false
 
 let unquote s =
-  if lang () <> Scheme then s
+  if lang () != Scheme then s
   else
     let s = String.copy s in
-    for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
+    for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done;
     s
 
 let rec qualify delim = function
@@ -112,14 +112,14 @@ let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id))
 let uppercase_id id =
   let s = string_of_id id in
-  assert (s<>"");
-  if s.[0] = '_' then Id.of_string ("Coq_"^s)
+  assert (not (String.is_empty s));
+  if s.[0] == '_' then Id.of_string ("Coq_"^s)
   else Id.of_string (String.capitalize s)
 
 type kind = Term | Type | Cons | Mod
 
 let upperkind = function
-  | Type -> lang () = Haskell
+  | Type -> lang () == Haskell
   | Term -> false
   | Cons | Mod -> true
 
@@ -162,7 +162,7 @@ let push_vars ids (db,avoid) =
 
 let get_db_name n (db,_) =
   let id = List.nth db (pred n) in
-  if id = dummy_name then Id.of_string "__" else id
+  if Id.equal id dummy_name then Id.of_string "__" else id
 
 
 (*S Renamings of global objects. *)
@@ -266,7 +266,7 @@ let pop_visible, push_visible, get_visible =
       | v :: vl ->
 	  vis := vl;
 	  (* we save the 1st-level-content of MPfile for later use *)
-	  if get_phase () = Impl && modular () && is_modfile v.mp
+	  if get_phase () == Impl && modular () && is_modfile v.mp
 	  then add_mpfiles_content v.mp v.content
   and push mp mps =
     vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis
@@ -285,7 +285,7 @@ struct
   type t = ModPath.t * Label.t
   let compare (mp1, l1) (mp2, l2) =
     let c = Label.compare l1 l2 in
-    if c = 0 then ModPath.compare mp1 mp2 else c
+    if Int.equal c 0 then ModPath.compare mp1 mp2 else c
 end
 
 module DupMap = Map.Make(DupOrd)
@@ -304,7 +304,7 @@ type reset_kind = AllButExternal | Everything
 
 let reset_renaming_tables flag =
   do_cleanup ();
-  if flag = Everything then clear_mpfiles_content ()
+  if flag == Everything then clear_mpfiles_content ()
 
 (*S Renaming functions *)
 
@@ -320,7 +320,7 @@ let modular_rename k id =
   in
   if not (is_ok s) ||
     (Id.Set.mem id (get_keywords ())) ||
-    (String.length s >= 4 && String.sub s 0 4 = prefix)
+    (String.length s >= 4 && String.equal (String.sub s 0 4) prefix)
   then prefix ^ s
   else s
 
@@ -350,17 +350,20 @@ let rec mp_renaming_fun mp = match mp with
   | _ when not (modular ()) && at_toplevel mp -> [""]
   | MPdot (mp,l) ->
       let lmp = mp_renaming mp in
-      if lmp = [""] then (modfstlev_rename l)::lmp
-      else (modular_rename Mod (Label.to_id l))::lmp
+      let mp = match lmp with
+      | [""] -> modfstlev_rename l
+      | _ -> modular_rename Mod (Label.to_id l)
+      in
+      mp ::lmp
   | MPbound mbid ->
       let s = modular_rename Mod (MBId.to_id mbid) in
       if not (params_ren_mem mp) then [s]
       else let i,_,_ = MBId.repr mbid in [s^"__"^string_of_int i]
   | MPfile _ ->
       assert (modular ()); (* see [at_toplevel] above *)
-      assert (get_phase () = Pre);
+      assert (get_phase () == Pre);
       let current_mpfile = (List.last (get_visible ())).mp in
-      if mp <> current_mpfile then mpfiles_add mp;
+      if not (ModPath.equal mp current_mpfile) then mpfiles_add mp;
       [string_of_modfile mp]
 
 (* ... and its version using a cache *)
@@ -377,15 +380,15 @@ and mp_renaming =
 let ref_renaming_fun (k,r) =
   let mp = modpath_of_r r in
   let l = mp_renaming mp in
-  let l = if lang () <> Ocaml && not (modular ()) then [""] else l in
+  let l = if lang () != Ocaml && not (modular ()) then [""] else l in
   let s =
     let idg = safe_basename_of_global r in
-    if l = [""] (* this happens only at toplevel of the monolithic case *)
-    then
+    match l with
+    | [""] -> (* this happens only at toplevel of the monolithic case *)
       let globs = Id.Set.elements (get_global_ids ()) in
       let id = next_ident_away (kindcase_id k idg) globs in
       string_of_id id
-    else modular_rename k idg
+    | _ -> modular_rename k idg
   in
   add_global_ids (Id.of_string s);
   s::l
@@ -406,7 +409,7 @@ let ref_renaming =
 
 let rec clash mem mp0 ks = function
   | [] -> false
-  | mp :: _ when mp = mp0 -> false
+  | mp :: _ when ModPath.equal mp mp0 -> false
   | mp :: _ when mem mp ks -> true
   | _ :: mpl -> clash mem mp0 ks mpl
 
@@ -416,15 +419,18 @@ let mpfiles_clash mp0 ks =
 
 let rec params_lookup mp0 ks = function
   | [] -> false
-  | param :: _ when mp0 = param -> true
+  | param :: _ when ModPath.equal mp0 param -> true
   | param :: params ->
-      if ks = (Mod, List.hd (mp_renaming param)) then params_ren_add param;
+      let () = match ks with
+      | (Mod, mp) when String.equal (List.hd (mp_renaming param)) mp -> params_ren_add param
+      | _ -> ()
+      in
       params_lookup mp0 ks params
 
 let visible_clash mp0 ks =
   let rec clash = function
     | [] -> false
-    | v :: _ when v.mp = mp0 -> false
+    | v :: _ when ModPath.equal v.mp mp0 -> false
     | v :: vis ->
 	let b = Hashtbl.mem v.content ks in
 	if b && not (is_mp_bound mp0) then true
@@ -440,7 +446,7 @@ let visible_clash mp0 ks =
 let visible_clash_dbg mp0 ks =
   let rec clash = function
     | [] -> None
-    | v :: _ when v.mp = mp0 -> None
+    | v :: _ when ModPath.equal v.mp mp0 -> None
     | v :: vis ->
 	try Some (v.mp,Hashtbl.find v.content ks)
 	with Not_found ->
@@ -483,7 +489,7 @@ let opened_libraries () =
 
 let pp_duplicate k' prefix mp rls olab =
   let rls', lbl =
-    if k'<>Mod then
+    if k' != Mod then
       (* Here rls=[s], the ref to print is <prefix>.<s>, and olab<>None *)
       rls, Option.get olab
     else
@@ -492,7 +498,7 @@ let pp_duplicate k' prefix mp rls olab =
   in
   try dottify (check_duplicate prefix lbl :: rls')
   with Not_found ->
-    assert (get_phase () = Pre); (* otherwise it's too late *)
+    assert (get_phase () == Pre); (* otherwise it's too late *)
     add_duplicate prefix lbl; dottify rls
 
 let fstlev_ks k = function
@@ -505,7 +511,7 @@ let fstlev_ks k = function
 
 let pp_ocaml_local k prefix mp rls olab =
   (* what is the largest prefix of [mp] that belongs to [visible]? *)
-  assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
+  assert (k != Mod || not (ModPath.equal mp prefix)); (* mp as whole module isn't in itself *)
   let rls' = List.skipn (mp_length prefix) rls in
   let k's = fstlev_ks k rls' in
   (* Reference r / module path mp is of the form [<prefix>.s.<...>]. *)
@@ -517,7 +523,7 @@ let pp_ocaml_local k prefix mp rls olab =
 
 let pp_ocaml_bound base rls =
   (* clash with a MPbound will be detected and fixed by renaming this MPbound *)
-  if get_phase () = Pre then ignore (visible_clash base (Mod,List.hd rls));
+  if get_phase () == Pre then ignore (visible_clash base (Mod,List.hd rls));
   dottify rls
 
 (* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *)
@@ -526,7 +532,7 @@ let pp_ocaml_extern k base rls = match rls with
   | [] -> assert false
   | base_s :: rls' ->
       if (not (modular ())) (* Pseudo qualification with "" *)
-	|| (rls' = [])  (* Case of a file A.v used as a module later *)
+	|| (List.is_empty rls')  (* Case of a file A.v used as a module later *)
 	|| (not (mpfiles_mem base)) (* Module not opened *)
 	|| (mpfiles_clash base (fstlev_ks k rls')) (* Conflict in opened files *)
 	|| (visible_clash base (fstlev_ks k rls')) (* Local conflict *)
@@ -556,7 +562,7 @@ let pp_haskell_gen k mp rls = match rls with
   | s::rls' ->
     let str = pseudo_qualify rls' in
     let str = if is_upper str && not (upperkind k) then ("_"^str) else str in
-    let prf = if base_mp mp <> top_visible_mp () then s ^ "." else "" in
+    let prf = if not (ModPath.equal (base_mp mp) (top_visible_mp ())) then s ^ "." else "" in
     prf ^ str
 
 (* Main name printing function for a reference *)
@@ -566,7 +572,7 @@ let pp_global k r =
   assert (List.length ls > 1);
   let s = List.hd ls in
   let mp,_,l = repr_of_r r in
-  if mp = top_visible_mp () then
+  if ModPath.equal mp (top_visible_mp ()) then
     (* simpliest situation: definition of r (or use in the same context) *)
     (* we update the visible environment *)
     (add_visible (k,s) l; unquote s)
@@ -582,7 +588,7 @@ let pp_global k r =
 let pp_module mp =
   let ls = mp_renaming mp in
   match mp with
-    | MPdot (mp0,l) when mp0 = top_visible_mp () ->
+    | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) ->
 	(* simpliest situation: definition of mp (or use in the same context) *)
 	(* we update the visible environment *)
 	let s = List.hd ls in
@@ -605,7 +611,7 @@ let check_extract_ascii () =
       | Haskell -> "Char"
       | _ -> raise Not_found
     in
-    find_custom (IndRef (ind_ascii,0)) = char_type
+    String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type)
   with Not_found -> false
 
 let is_list_cons l =
@@ -613,7 +619,7 @@ let is_list_cons l =
 
 let is_native_char = function
   | MLcons(_,ConstructRef ((kn,0),1),l) ->
-    kn = ind_ascii && check_extract_ascii () && is_list_cons l
+    MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l
   | _ -> false
 
 let pp_native_char c =