Removing a bunch of generic equalities.

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

9 files changed, 261 insertions, 233 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 =
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index f57832d3f..5f17e0997 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -52,14 +52,15 @@ let toplevel_env () =
 
 let environment_until dir_opt =
   let rec parse = function
-    | [] when dir_opt = None -> [Lib.current_mp (), toplevel_env ()]
+    | [] when Option.is_empty dir_opt -> [Lib.current_mp (), toplevel_env ()]
     | [] -> []
     | d :: l ->
       let meb =
         Modops.destr_nofunctor (Global.lookup_module (MPfile d)).mod_type
       in
-      if dir_opt = Some d then [MPfile d, meb]
-      else (MPfile d, meb) :: (parse l)
+      match dir_opt with
+      | Some d' when DirPath.equal d d' -> [MPfile d, meb]
+      | _ -> (MPfile d, meb) :: (parse l)
   in parse (Library.loaded_libraries ())
 
 
@@ -137,20 +138,20 @@ let check_fix env cb i =
   match cb.const_body with
     | Def lbody ->
 	(match kind_of_term (Lazyconstr.force lbody) with
-	  | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd)
-	  | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd)
+	  | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
+	  | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
 	  | _ -> raise Impossible)
     | Undef _ | OpaqueDef _ -> raise Impossible
 
 let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) =
-  na1 = na2 &&
+  Array.equal Name.equal na1 na2 &&
   Array.equal eq_constr ca1 ca2 &&
   Array.equal eq_constr ta1 ta2
 
 let factor_fix env l cb msb =
   let _,recd as check = check_fix env cb 0 in
   let n = Array.length (let fi,_,_ = recd in fi) in
-  if n = 1 then [|l|], recd, msb
+  if Int.equal n 1 then [|l|], recd, msb
   else begin
     if List.length msb < n-1 then raise Impossible;
     let msb', msb'' = List.chop (n-1) msb in
@@ -160,7 +161,7 @@ let factor_fix env l cb msb =
 	 function
 	   | (l,SFBconst cb') ->
 	       let check' = check_fix env cb' (j+1) in
-	       if not (fst check = fst check' &&
+	       if not ((fst check : bool) == (fst check') &&
 		   prec_declaration_equal (snd check) (snd check'))
 	       then raise Impossible;
 	       labels.(j+1) <- l;
@@ -324,7 +325,7 @@ let rec extract_structure env mp all = function
 
 and extract_mexpr env mp all = function
   | MEwith _ -> assert false (* no 'with' syntax for modules *)
-  | me when lang () <> Ocaml ->
+  | me when lang () != Ocaml ->
       (* in Haskell/Scheme, we expand everything *)
       extract_msignature env mp all (expand_mexpr env mp me)
   | MEident mp ->
@@ -408,7 +409,7 @@ let mono_filename f =
 	  else f
 	in
 	let id =
-	  if lang () <> Haskell then default_id
+	  if lang () != Haskell then default_id
 	  else
             try Id.of_string (Filename.basename f)
 	    with UserError _ ->
@@ -464,7 +465,7 @@ let formatter dry file =
 
 let get_comment () =
   let s = file_comment () in
-  if s = "" then None
+  if String.is_empty s then None
   else
     let split_comment = Str.split (Str.regexp "[ \t\n]+") s in
     Some (prlist_with_sep spc str split_comment)
@@ -474,11 +475,11 @@ let print_structure_to_file (fn,si,mo) dry struc =
   let d = descr () in
   reset_renaming_tables AllButExternal;
   let unsafe_needs = {
-    mldummy = struct_ast_search ((=) MLdummy) struc;
+    mldummy = struct_ast_search ((==) MLdummy) struc;
     tdummy = struct_type_search Mlutil.isDummy struc;
-    tunknown = struct_type_search ((=) Tunknown) struc;
+    tunknown = struct_type_search ((==) Tunknown) struc;
     magic =
-      if lang () <> Haskell then false
+      if lang () != Haskell then false
       else struct_ast_search (function MLmagic _ -> true | _ -> false) struc }
   in
   (* First, a dry run, for computing objects to rename or duplicate *)
@@ -516,7 +517,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
        info_file si)
     (if dry then None else si);
   (* Print the buffer content via Coq standard formatter (ok with coqide). *)
-  if Buffer.length buf <> 0 then begin
+  if not (Int.equal (Buffer.length buf) 0) then begin
     Pp.msg_info (str (Buffer.contents buf));
     Buffer.reset buf
   end
@@ -536,7 +537,7 @@ let init modular library =
   set_modular modular;
   set_library library;
   reset ();
-  if modular && lang () = Scheme then error_scheme ()
+  if modular && lang () == Scheme then error_scheme ()
 
 let warns () =
   warning_opaques (access_opaque ());
@@ -637,7 +638,7 @@ let extraction_library is_rec m =
   warns ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
-	let dry = not is_rec && dir <> dir_m in
+	let dry = not is_rec && not (DirPath.equal dir dir_m) in
 	print_structure_to_file (module_filename mp) dry [e]
     | _ -> assert false
   in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6c1be2d36..947a1a482 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -37,13 +37,13 @@ let none = Evd.empty
 
 let type_of env c =
   try
-    let polyprop = (lang() = Haskell) in
+    let polyprop = (lang() == Haskell) in
     Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
   with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
 let sort_of env c =
   try
-    let polyprop = (lang() = Haskell) in
+    let polyprop = (lang() == Haskell) in
     Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
   with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
@@ -78,11 +78,13 @@ let rec flag_of_type env t : flag =
     | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
     | Sort (Prop Null) -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
-    | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default)
+    | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default)
 
 (*s Two particular cases of [flag_of_type]. *)
 
-let is_default env t = (flag_of_type env t = (Info, Default))
+let is_default env t = match flag_of_type env t with
+| (Info, Default) -> true
+| _ -> false
 
 exception NotDefault of kill_reason
 
@@ -92,7 +94,9 @@ let check_default env t =
     | Logic,_ -> raise (NotDefault Kother)
     | _ -> ()
 
-let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
+let is_info_scheme env t = match flag_of_type env t with
+| (Info, TypeScheme) -> true
+| _ -> false
 
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
@@ -137,7 +141,7 @@ let sign_with_implicits r s nb_params =
     | [] -> []
     | sign::s ->
 	let sign' =
-	  if sign = Keep && List.mem i implicits then Kill Kother else sign
+	  if sign == Keep && List.mem i implicits then Kill Kother else sign
 	in sign' :: add_impl (succ i) s
   in
   add_impl (1+nb_params) s
@@ -171,7 +175,7 @@ let db_from_sign s =
   an inductive type (see just below). *)
 
 let rec db_from_ind dbmap i =
-  if i = 0 then []
+  if Int.equal i 0 then []
   else (try Int.Map.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
 
 (*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument
@@ -195,25 +199,25 @@ let parse_ind_args si args relmax =
   in parse 1 1 si
 
 let oib_equal o1 o2 =
-  Id.compare o1.mind_typename o2.mind_typename = 0 &&
+  Id.equal o1.mind_typename o2.mind_typename &&
   List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
   begin match o1.mind_arity, o2.mind_arity with
   | Monomorphic {mind_user_arity=c1; mind_sort=s1},
     Monomorphic {mind_user_arity=c2; mind_sort=s2} ->
-      eq_constr c1 c2 && s1 = s2
-  | ma1, ma2 -> ma1 = ma2 end &&
-  o1.mind_consnames = o2.mind_consnames
+      eq_constr c1 c2 && Sorts.equal s1 s2
+  | ma1, ma2 -> Pervasives.(=) ma1 ma2 (** FIXME: this one is surely wrong *) end &&
+    Array.equal Id.equal o1.mind_consnames o2.mind_consnames
 
 let mib_equal m1 m2 =
   Array.equal oib_equal m1.mind_packets m1.mind_packets &&
-  m1.mind_record = m2.mind_record &&
-  m1.mind_finite = m2.mind_finite &&
-  m1.mind_ntypes = m2.mind_ntypes &&
+  (m1.mind_record : bool) == m2.mind_record &&
+  (m1.mind_finite : bool) == m2.mind_finite &&
+  Int.equal m1.mind_ntypes m2.mind_ntypes &&
   List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
-  m1.mind_nparams = m2.mind_nparams &&
-  m1.mind_nparams_rec = m2.mind_nparams_rec &&
+  Int.equal m1.mind_nparams m2.mind_nparams &&
+  Int.equal m1.mind_nparams_rec m2.mind_nparams_rec &&
   List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
-  m1.mind_constraints = m2.mind_constraints
+  Pervasives.(=) m1.mind_constraints m2.mind_constraints (** FIXME *)
 
 (*S Extraction of a type. *)
 
@@ -236,7 +240,7 @@ let rec extract_type env db j c args =
 	   | [] -> assert false (* A lambda cannot be a type. *)
 	   | a :: args -> extract_type env db j (subst1 a d) args)
     | Prod (n,t,d) ->
-	assert (args = []);
+	assert (List.is_empty args);
 	let env' = push_rel_assum (n,t) env in
 	(match flag_of_type env t with
 	   | (Info, Default) ->
@@ -256,10 +260,10 @@ let rec extract_type env db j c args =
 	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
 		  | _ ->
-		      let reason = if lvl=TypeScheme then Ktype else Kother in
+		      let reason = if lvl == TypeScheme then Ktype else Kother in
 		      Tarr (Tdummy reason, mld)))
     | Sort _ -> Tdummy Ktype (* The two logical cases. *)
-    | _ when sort_of env (applist (c, args)) = InProp -> Tdummy Kother
+    | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kother
     | Rel n ->
 	(match lookup_rel n env with
            | (_,Some t,_) -> extract_type env db j (lift n t) args
@@ -267,7 +271,7 @@ let rec extract_type env db j c args =
 	       (* Asks [db] a translation for [n]. *)
 	       if n > List.length db then Tunknown
 	       else let n' = List.nth db (n-1) in
-	       if n' = 0 then Tunknown else Tvar n')
+	       if Int.equal n' 0 then Tunknown else Tvar n')
     | Const kn ->
 	let r = ConstRef kn in
 	let cb = lookup_constant kn env in
@@ -287,7 +291,7 @@ let rec extract_type env db j c args =
 		      (* The more precise is [mlt'], extracted after reduction *)
 		      (* The shortest is [mlt], which use abbreviations *)
 		      (* If possible, we take [mlt], otherwise [mlt']. *)
-		      if expand env mlt = expand env mlt' then mlt else mlt')
+		      if Pervasives.(=) (expand env mlt) (expand env mlt') then mlt else mlt') (** FIXME *)
 	   | (Info, Default) ->
                (* Not an ML type, for example [(c:forall X, X->X) Type nat] *)
 	       (match cb.const_body with
@@ -309,7 +313,7 @@ let rec extract_type env db j c args =
 and extract_type_app env db (r,s) args =
   let ml_args =
     List.fold_right
-      (fun (b,c) a -> if b=Keep then
+      (fun (b,c) a -> if b == Keep then
 	 let p = List.length (fst (splay_prod env none (type_of env c))) in
          let db = iterate (fun l -> 0 :: l) p db in
          (extract_type_scheme env db c p) :: a
@@ -327,7 +331,7 @@ and extract_type_app env db (r,s) args =
 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
 and extract_type_scheme env db c p =
-  if p=0 then extract_type env db 0 c []
+  if Int.equal p 0 then extract_type env db 0 c []
   else
     let c = whd_betaiotazeta Evd.empty c in
     match kind_of_term c with
@@ -357,9 +361,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
        When at toplevel of the monolithic case, we cannot do much
        (cf Vector and bug #2570) *)
     let equiv =
-      if lang () <> Ocaml ||
+      if lang () != Ocaml ||
 	 (not (modular ()) && at_toplevel (mind_modpath kn)) ||
-	 kn_ord (canonical_mind kn) (user_mind kn) = 0
+	 KerName.equal (canonical_mind kn) (user_mind kn)
       then
 	NoEquiv
       else
@@ -379,7 +383,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
       Array.mapi
 	(fun i mip ->
 	   let ar = Inductive.type_of_inductive env (mib,mip) in
-	   let info = (fst (flag_of_type env ar) = Info) in
+	   let info = (fst (flag_of_type env ar) == Info) in
 	   let s,v = if info then type_sign_vl env ar else [],[] in
 	   let t = Array.make (Array.length mip.mind_nf_lc) [] in
 	   { ip_typename = mip.mind_typename;
@@ -422,16 +426,16 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	let r = IndRef ip in
 	if is_custom r then raise (I Standard);
 	if not mib.mind_finite then raise (I Coinductive);
-	if mib.mind_ntypes <> 1 then raise (I Standard);
+	if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
 	let p = packets.(0) in
 	if p.ip_logical then raise (I Standard);
-	if Array.length p.ip_types <> 1 then raise (I Standard);
+	if not (Int.equal (Array.length p.ip_types) 1) then raise (I Standard);
 	let typ = p.ip_types.(0) in
 	let l = List.filter (fun t -> not (isDummy (expand env t))) typ in
 	if not (keep_singleton ()) &&
-	    List.length l = 1 && not (type_mem_kn kn (List.hd l))
+	    Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l))
 	then raise (I Singleton);
-	if l = [] then raise (I Standard);
+	if List.is_empty l then raise (I Standard);
 	if not mib.mind_record then raise (I Standard);
 	(* Now we're sure it's a record. *)
 	(* First, we find its field names. *)
@@ -443,7 +447,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	in
 	let field_names =
 	  List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
-	assert (List.length field_names = List.length typ);
+	assert (Int.equal (List.length field_names) (List.length typ));
 	let projs = ref Cset.empty in
 	let mp = MutInd.modpath kn in
 	let rec select_fields l typs = match l,typs with
@@ -455,7 +459,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | Name id::l, typ::typs ->
 	      let knp = Constant.make2 mp (Label.of_id id) in
 	      (* Is it safe to use [id] for projections [foo.id] ? *)
-	      if List.for_all ((=) Keep) (type2signature env typ)
+	      if List.for_all ((==) Keep) (type2signature env typ)
 	      then projs := Cset.add knp !projs;
 	      Some (ConstRef knp) :: (select_fields l typs)
 	  | _ -> assert false
@@ -653,7 +657,7 @@ and extract_cst_app env mle mlt kn args =
   (* Can we instantiate types variables for this constant ? *)
   (* In Ocaml, inside the definition of this constant, the answer is no. *)
   let instantiated =
-    if lang () = Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema)
+    if lang () == Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema)
     else instantiation schema
   in
   (* Then the expected type of this constant. *)
@@ -675,14 +679,14 @@ and extract_cst_app env mle mlt kn args =
   (* The ml arguments, already expunged from known logical ones *)
   let mla = make_mlargs env mle s args metas in
   let mla =
-    if magic1 || lang () <> Ocaml then mla
+    if magic1 || lang () != Ocaml then mla
     else
       try
         (* for better optimisations later, we discard dependent args
            of projections and replace them by fake args that will be
            removed during final pretty-print. *)
 	let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
-	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
+	if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
       with e when Errors.noncritical e -> mla
   in
@@ -690,7 +694,7 @@ and extract_cst_app env mle mlt kn args =
      one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
      accordingly. *)
   let optdummy = match sign_kind s_full with
-    | UnsafeLogicalSig when lang () <> Haskell -> [MLdummy]
+    | UnsafeLogicalSig when lang () != Haskell -> [MLdummy]
     | _ -> []
   in
   (* Different situations depending of the number of arguments: *)
@@ -743,7 +747,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
   let magic2 = needs_magic (a, mlt) in
   let head mla =
-    if mi.ind_kind = Singleton then
+    if mi.ind_kind == Singleton then
       put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
     else
       let typeargs = match snd (type_decomp type_cons) with
@@ -760,7 +764,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
       (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
   else
     let mla = make_mlargs env mle s args' metas in
-    if la = ls + params_nb
+    if Int.equal la (ls + params_nb)
     then put_magic_if (magic2 && not magic1) (head mla)
     else (* [ params_nb <= la <= ls + params_nb ] *)
       let ls' = params_nb + ls - la in
@@ -775,20 +779,20 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
   (* [ni]: number of arguments without parameters in each branch *)
   let ni = mis_constr_nargs_env env ip in
   let br_size = Array.length br in
-  assert (Array.length ni = br_size);
-  if br_size = 0 then begin
+  assert (Int.equal (Array.length ni) br_size);
+  if Int.equal br_size 0 then begin
     add_recursors env kn; (* May have passed unseen if logical ... *)
     MLexn "absurd case"
   end else
     (* [c] has an inductive type, and is not a type scheme type. *)
     let t = type_of env c in
     (* The only non-informative case: [c] is of sort [Prop] *)
-    if (sort_of env t) = InProp then
+    if (sort_of env t) == InProp then
       begin
 	add_recursors env kn; (* May have passed unseen if logical ... *)
 	(* Logical singleton case: *)
 	(* [match c with C i j k -> t] becomes [t'] *)
-	assert (br_size = 1);
+	assert (Int.equal br_size 1);
 	let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in
 	let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in
 	let e = extract_maybe_term env mle mlt br.(0) in
@@ -817,13 +821,13 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
 	(List.rev ids, Pusual r, e')
       in
-      if mi.ind_kind = Singleton then
+      if mi.ind_kind == Singleton then
 	begin
 	  (* Informative singleton case: *)
 	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
-	  assert (br_size = 1);
+	  assert (Int.equal br_size 1);
 	  let (ids,_,e') = extract_branch 0 in
-	  assert (List.length ids = 1);
+	  assert (Int.equal (List.length ids) 1);
 	  MLletin (tmp_id (List.hd ids),a,e')
 	end
       else
@@ -893,8 +897,8 @@ let extract_std_constant env kn body typ =
     if n <= m then decompose_lam_n n body
     else
       let s,s' = List.chop m s in
-      if List.for_all ((=) Keep) s' &&
-	(lang () = Haskell || sign_kind s <> UnsafeLogicalSig)
+      if List.for_all ((==) Keep) s' &&
+	(lang () == Haskell || sign_kind s != UnsafeLogicalSig)
       then decompose_lam_n m body
       else decomp_lams_eta_n n m env body typ
   in
@@ -903,9 +907,9 @@ let extract_std_constant env kn body typ =
     let n = List.length rels in
     let s,s' = List.chop n s in
     let k = sign_kind s in
-    let empty_s = (k = EmptySig || k = SafeLogicalSig) in
-    if lang () = Ocaml && empty_s && not (gentypvar_ok c)
-      && s' <> [] && type_maxvar t <> 0
+    let empty_s = (k == EmptySig || k == SafeLogicalSig) in
+    if lang () == Ocaml && empty_s && not (gentypvar_ok c)
+      && not (List.is_empty s') && not (Int.equal (type_maxvar t) 0)
     then decomp_lams_eta_n (n+1) n env body typ
     else rels,c
   in
@@ -949,7 +953,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
   let sub = List.rev_map mkConst kns in
   for i = 0 to n-1 do
-    if sort_of env ti.(i) <> InProp then begin
+    if sort_of env ti.(i) != InProp then begin
       let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
       terms.(i) <- e;
       types.(i) <- t;
@@ -1059,7 +1063,7 @@ let logical_decl = function
   | Dterm (_,MLdummy,Tdummy _) -> true
   | Dtype (_,[],Tdummy _) -> true
   | Dfix (_,av,tv) ->
-      (Array.for_all ((=) MLdummy) av) &&
+      (Array.for_all ((==) MLdummy) av) &&
       (Array.for_all isDummy tv)
   | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 59dd5596e..86681e370 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -51,7 +51,7 @@ let preamble mod_name comment used_modules usf =
   str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++
   str "import qualified Prelude" ++ fnl () ++
   prlist pp_import used_modules ++ fnl () ++
-  (if used_modules = [] then mt () else fnl ()) ++
+  (if List.is_empty used_modules then mt () else fnl ()) ++
   (if not usf.magic then mt ()
    else str "\
 \nunsafeCoerce :: a -> b\
@@ -91,7 +91,7 @@ let rec pp_type par vl t =
        with Failure _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
     | Tglob (IndRef(kn,0),l)
-	when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->
+	when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
 	  pp_type true vl (List.hd l)
     | Tglob (r,l) ->
 	  pp_par par
@@ -145,7 +145,7 @@ let rec pp_expr par env args =
     | MLglob r ->
 	apply (pp_global Term r)
     | MLcons (_,r,a) as c ->
-        assert (args=[]);
+        assert (List.is_empty args);
         begin match a with
 	  | _ when is_native_char c -> pp_native_char c
 	  | [] -> pp_global Cons r
@@ -156,13 +156,13 @@ let rec pp_expr par env args =
 			prlist_with_sep spc (pp_expr true env []) a)
 	end
     | MLtuple l ->
-        assert (args=[]);
+        assert (List.is_empty args);
         pp_boxed_tuple (pp_expr true env []) l
     | MLcase (_,t, pv) when is_custom_match pv ->
         if not (is_regular_match pv) then
 	  error "Cannot mix yet user-given match and general patterns.";
 	let mkfun (ids,_,e) =
-	  if ids <> [] then named_lams (List.rev ids) e
+	  if not (List.is_empty ids) then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
 	in
 	let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in
@@ -190,7 +190,7 @@ let rec pp_expr par env args =
 
 and pp_cons_pat par r ppl =
   pp_par par
-    (pp_global Cons r ++ space_if (ppl<>[]) ++ prlist_with_sep spc identity ppl)
+    (pp_global Cons r ++ space_if (not (List.is_empty ppl)) ++ prlist_with_sep spc identity ppl)
 
 and pp_gen_pat par ids env = function
   | Pcons (r,l) -> pp_cons_pat par r (List.map (pp_gen_pat true ids env) l)
@@ -210,7 +210,7 @@ and pp_pat env pv =
   prvecti
     (fun i x ->
        pp_one_pat env pv.(i) ++
-       if i = Array.length pv - 1 then str "}" else
+       if Int.equal i (Array.length pv - 1) then str "}" else
 	 (str ";" ++ fnl ()))
     pv
 
@@ -246,7 +246,7 @@ let pp_singleton kn packet =
   let l' = List.rev l in
   hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++
 	 prlist_with_sep spc pr_id l ++
-	 (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++
+	 (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++
 	 pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++
 		     pr_id packet.ip_consnames.(0)))
@@ -261,10 +261,10 @@ let pp_one_ind ip pl cv =
       	       	prlist_with_sep
 		  (fun () -> (str " ")) (pp_type true pl) l))
   in
-  str (if Array.length cv = 0 then "type " else "data ") ++
+  str (if Array.is_empty cv then "type " else "data ") ++
   pp_global Type (IndRef ip) ++
   prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++
-  if Array.length cv = 0 then str " () -- empty inductive"
+  if Array.is_empty cv then str " () -- empty inductive"
   else
     (fnl () ++ str " " ++
      v 0 (str "  " ++
@@ -289,7 +289,7 @@ let rec pp_ind first kn i ind =
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
-  | Dind (kn,i) when i.ind_kind = Singleton ->
+  | Dind (kn,i) when i.ind_kind == Singleton ->
       pp_singleton kn i.ind_packets.(0) ++ fnl ()
   | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i)
   | Dtype (r, l, t) ->
@@ -302,7 +302,7 @@ let pp_decl = function
 	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
 	  with Not_found ->
 	    prlist (fun id -> pr_id id ++ str " ") l ++
-	    if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
+	    if t == Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
 	    else str "=" ++ spc () ++ pp_type false l t
 	in
 	hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 ()
@@ -313,7 +313,7 @@ let pp_decl = function
       prvecti
 	(fun i r ->
 	  let void = is_inline_custom r ||
-	    (not (is_custom r) && defs.(i) = MLexn "UNUSED")
+	    (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
 	  in
 	  if void then mt ()
 	  else
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 4ad681c05..1e6a1fffc 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -29,7 +29,7 @@ let anonymous = Id anonymous_name
 
 let id_of_name = function
   | Anonymous -> anonymous_name
-  | Name id when id = dummy_name -> anonymous_name
+  | Name id when Id.equal id dummy_name -> anonymous_name
   | Name id -> id
 
 let id_of_mlid = function
@@ -85,7 +85,7 @@ let instantiation (nb,t) = type_subst_vect (Array.init nb new_meta) t
 
 let rec type_occurs alpha t =
   match t with
-  | Tmeta {id=beta; contents=None} -> alpha = beta
+  | Tmeta {id=beta; contents=None} -> Int.equal alpha beta
   | Tmeta {contents=Some u} -> type_occurs alpha u
   | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
   | Tglob (r,l) -> List.exists (type_occurs alpha) l
@@ -94,7 +94,7 @@ let rec type_occurs alpha t =
 (*s Most General Unificator *)
 
 let rec mgu = function
-  | Tmeta m, Tmeta m' when m.id = m'.id -> ()
+  | Tmeta m, Tmeta m' when Int.equal m.id m'.id -> ()
   | Tmeta m, t | t, Tmeta m ->
     (match m.contents with
       | Some u -> mgu (u, t)
@@ -102,21 +102,24 @@ let rec mgu = function
       | None -> m.contents <- Some t)
   | Tarr(a, b), Tarr(a', b') ->
       mgu (a, a'); mgu (b, b')
-  | Tglob (r,l), Tglob (r',l') when r = r' ->
+  | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
        List.iter mgu (List.combine l l')
-  | (Tdummy _, _ | _, Tdummy _) when lang() = Haskell -> ()
+  | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> ()
   | Tdummy _, Tdummy _ -> ()
-  | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
+  | Tvar i, Tvar j when Int.equal i j -> ()
+  | Tvar' i, Tvar' j when  Int.equal i j -> ()
+  | Tunknown, Tunknown -> ()
+  | Taxiom, Taxiom -> ()
   | _ -> raise Impossible
 
 let needs_magic p = try mgu p; false with Impossible -> true
 
-let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
+let put_magic_if b a = if b && lang () != Scheme then MLmagic a else a
 
-let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
+let put_magic p a = if needs_magic p && lang () != Scheme then MLmagic a else a
 
 let generalizable a =
-  lang () <> Ocaml ||
+  lang () != Ocaml ||
     match a with
       | MLapp _ -> false
       | _ -> true (* TODO, this is just an approximation for the moment *)
@@ -147,7 +150,7 @@ module Mlenv = struct
   (* [find_free] finds the free meta in a type. *)
 
   let rec find_free set = function
-    | Tmeta m when m.contents = None -> Metaset.add m set
+    | Tmeta m when Option.is_empty m.contents -> Metaset.add m set
     | Tmeta {contents = Some t} -> find_free set t
     | Tarr (a,b) -> find_free (find_free set a) b
     | Tglob (_,l) -> List.fold_left find_free set l
@@ -302,7 +305,7 @@ let rec sign_kind = function
 	| NonLogicalSig -> NonLogicalSig
 	| UnsafeLogicalSig -> UnsafeLogicalSig
 	| SafeLogicalSig | EmptySig ->
-	    if k = Kother then UnsafeLogicalSig else SafeLogicalSig
+	    if k == Kother then UnsafeLogicalSig else SafeLogicalSig
 
 (* Removing the final [Keep] in a signature *)
 
@@ -310,17 +313,17 @@ let rec sign_no_final_keeps = function
   | [] -> []
   | k :: s ->
       let s' = k :: sign_no_final_keeps s in
-      if s' = [Keep] then [] else s'
+      match s' with [Keep] -> [] | _ -> s'
 
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
 let type_expunge_from_sign env s t =
   let rec expunge s t =
-    if s = [] then t else match t with
+    if List.is_empty s then t else match t with
       | Tmeta {contents = Some t} -> expunge s t
       | Tarr (a,b) ->
 	  let t = expunge (List.tl s) b in
-	  if List.hd s = Keep then Tarr (a, t) else t
+	  if List.hd s == Keep then Tarr (a, t) else t
       | Tglob (r,l) ->
 	  (match env r with
 	     | Some mlt -> expunge s (type_subst_list l mlt)
@@ -328,7 +331,7 @@ let type_expunge_from_sign env s t =
       | _ -> assert false
   in
   let t = expunge (sign_no_final_keeps s) t in
-  if lang () <> Haskell && sign_kind s = UnsafeLogicalSig then
+  if lang () != Haskell && sign_kind s == UnsafeLogicalSig then
     Tarr (Tdummy Kother, t)
   else t
 
@@ -337,7 +340,7 @@ let type_expunge env t =
 
 (*S Generic functions over ML ast terms. *)
 
-let mlapp f a = if a = [] then f else MLapp (f,a)
+let mlapp f a = if List.is_empty a then f else MLapp (f,a)
 
 (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care
    of the number of bingings crossed before reaching the [MLrel]. *)
@@ -412,7 +415,7 @@ let ast_iter f = function
 
 let ast_occurs k t =
   try
-    ast_iter_rel (fun i -> if i = k then raise Found) t; false
+    ast_iter_rel (fun i -> if Int.equal i k then raise Found) t; false
   with Found -> true
 
 (*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)]
@@ -428,7 +431,7 @@ let ast_occurs_itvl k k' t =
 
 let nb_occur_match =
   let rec nb k = function
-    | MLrel i -> if i = k then 1 else 0
+    | MLrel i -> if Int.equal i k then 1 else 0
     | MLcase(_,a,v) ->
         (nb k a) +
 	Array.fold_left
@@ -450,7 +453,7 @@ let ast_lift k t =
   let rec liftrec n = function
     | MLrel i as a -> if i-n < 1 then a else MLrel (i+k)
     | a -> ast_map_lift liftrec n a
-  in if k = 0 then t else liftrec 0 t
+  in if Int.equal k 0 then t else liftrec 0 t
 
 let ast_pop t = ast_lift (-1) t
 
@@ -474,7 +477,7 @@ let ast_subst e =
   let rec subst n = function
     | MLrel i as a ->
 	let i' = i-n in
-	if i'=1 then ast_lift n e
+	if Int.equal i' 1 then ast_lift n e
 	else if i'<1 then a
 	else MLrel (i-1)
     | a -> ast_map_lift subst n a
@@ -512,14 +515,15 @@ let has_deep_pattern br =
   Array.exists (function (_,pat,_) -> deep pat) br
 
 let is_regular_match br =
-  if Array.length br = 0 then false (* empty match becomes MLexn *)
+  if Array.is_empty br then false (* empty match becomes MLexn *)
   else
     try
       let get_r (ids,pat,c) =
 	match pat with
 	  | Pusual r -> r
 	  | Pcons (r,l) ->
-	    if not (List.for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
+            let is_rel i = function Prel j -> Int.equal i j | _ -> false in
+	    if not (List.for_all_i is_rel 1 (List.rev l))
 	    then raise Impossible;
 	    r
 	  | _ -> raise Impossible
@@ -528,7 +532,11 @@ let is_regular_match br =
 	| ConstructRef (ind,_) -> ind
 	| _ -> raise Impossible
       in
-      Array.for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br
+      let is_ref i tr = match get_r tr with
+      | ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1)
+      | _ -> false
+      in
+      Array.for_all_i is_ref 0 br
     with Impossible -> false
 
 (*S Operations concerning lambdas. *)
@@ -546,7 +554,7 @@ let collect_lams =
 
 let collect_n_lams =
   let rec collect acc n t =
-    if n = 0 then acc,t
+    if Int.equal n 0 then acc,t
     else match t with
       | MLlam(id,t) -> collect (id::acc) (n-1) t
       | _ -> assert false
@@ -555,7 +563,7 @@ let collect_n_lams =
 (*s [remove_n_lams] just removes some [MLlam]. *)
 
 let rec remove_n_lams n t =
-  if n = 0 then t
+  if Int.equal n 0 then t
   else match t with
       | MLlam(_,t) -> remove_n_lams (n-1) t
       | _ -> assert false
@@ -593,7 +601,7 @@ let rec anonym_or_dummy_lams a = function
 (*s The following function creates [MLrel n;...;MLrel 1] *)
 
 let rec eta_args n =
-  if n = 0 then [] else (MLrel n)::(eta_args (pred n))
+  if Int.equal n 0 then [] else (MLrel n)::(eta_args (pred n))
 
 (*s Same, but filtered by a signature. *)
 
@@ -605,20 +613,21 @@ let rec eta_args_sign n = function
 (*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
 
 let rec test_eta_args_lift k n = function
-  | [] -> n=0
-  | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q)
+  | [] -> Int.equal n 0
+  | MLrel m :: q -> Int.equal (k+n) m && (test_eta_args_lift k (pred n) q)
+  | _ -> false
 
 (*s Computes an eta-reduction. *)
 
 let eta_red e =
   let ids,t = collect_lams e in
   let n = List.length ids in
-  if n = 0 then e
+  if Int.equal n 0 then e
   else match t with
     | MLapp (f,a) ->
 	let m = List.length a in
 	let ids,body,args =
-	  if m = n then
+	  if Int.equal m n then
 	    [], f, a
 	  else if m < n then
 	    List.skipn m ids, f, a
@@ -699,7 +708,7 @@ let branch_as_fun typ (l,p,c) =
 	if i'<1 then c
 	else if i'>nargs then MLrel (i-nargs+1)
 	else raise Impossible
-    | MLcons _ as cons' when cons' = ast_lift n cons -> MLrel (n+1)
+    | MLcons _ as cons' when Pervasives.(=) cons' (ast_lift n cons) -> MLrel (n+1) (*FIXME*)
     | a -> ast_map_lift genrec n a
   in genrec 0 c
 
@@ -767,7 +776,7 @@ let factor_branches o typ br =
     let br_factor, br_set = census_max MLdummy in
     census_clean ();
     let n = Int.Set.cardinal br_set in
-    if n = 0 then None
+    if Int.equal n 0 then None
     else if Array.length br >= 2 && n < 2 then None
     else Some (br_factor, br_set)
   end
@@ -778,7 +787,7 @@ let rec merge_ids ids ids' = match ids,ids' with
   | [],l -> l
   | l,[] -> l
   | i::ids, i'::ids' ->
-      (if i = Dummy then i' else i) :: (merge_ids ids ids')
+      (if i == Dummy then i' else i) :: (merge_ids ids ids')
 
 let is_exn = function MLexn _ -> true | _ -> false
 
@@ -788,7 +797,7 @@ let permut_case_fun br acc =
 		let ids, c = collect_lams t in
 		let n = List.length ids in
 		if (n < !nb) && (not (is_exn c)) then nb := n) br;
-  if !nb = max_int || !nb = 0 then ([],br)
+  if Int.equal !nb  max_int || Int.equal !nb 0 then ([],br)
   else begin
     let br = Array.copy br in
     let ids = ref [] in
@@ -821,16 +830,16 @@ let rec iota_red i lift br ((typ,r,a) as cons) =
   if i >= Array.length br then raise Impossible;
   let (ids,p,c) = br.(i) in
   match p with
-    | Pusual r' | Pcons (r',_) when r'<>r -> iota_red (i+1) lift br cons
+    | Pusual r' | Pcons (r',_) when not (Globnames.eq_gr r' r) -> iota_red (i+1) lift br cons
     | Pusual r' ->
       let c = named_lams (List.rev ids) c in
       let c = ast_lift lift c
       in MLapp (c,a)
-    | Prel 1 when List.length ids = 1 ->
+    | Prel 1 when Int.equal (List.length ids) 1 ->
       let c = MLlam (List.hd ids, c) in
       let c = ast_lift lift c
       in MLapp(c,[MLcons(typ,r,a)])
-    | Pwild when ids = [] -> ast_lift lift c
+    | Pwild when List.is_empty ids -> ast_lift lift c
     | _ -> raise Impossible (* TODO: handle some more cases *)
 
 (* [iota_gen] is an extension of [iota_red] where we allow to
@@ -881,7 +890,7 @@ let rec simpl o = function
       if
 	(is_atomic c) || (is_atomic e) ||
 	(let n = nb_occur_match e in
-	 (n = 0 || (n=1 && expand_linear_let o id e)))
+	 (Int.equal n 0 || (Int.equal n 1 && expand_linear_let o id e)))
       then
 	simpl o (ast_subst c e)
       else
@@ -934,14 +943,14 @@ and simpl_case o typ br e =
     (* Swap the case and the lam if possible *)
     let ids,br = if o.opt_case_fun then permut_case_fun br [] else [],br in
     let n = List.length ids in
-    if n <> 0 then
+    if not (Int.equal n 0) then
       simpl o (named_lams ids (MLcase (typ, ast_lift n e, br)))
     else
       (* Can we merge several branches as the same constant or function ? *)
-      if lang() = Scheme || is_custom_match br
+      if lang() == Scheme || is_custom_match br
       then MLcase (typ, e, br)
       else match factor_branches o typ br with
-	| Some (f,ints) when Int.Set.cardinal ints = Array.length br ->
+	| Some (f,ints) when Int.equal (Int.Set.cardinal ints) (Array.length br) ->
 	  (* If all branches have been factorized, we remove the match *)
 	  simpl o (MLletin (Tmp anonymous_name, e, f))
 	| Some (f,ints) ->
@@ -976,9 +985,9 @@ let rec select_via_bl l args = match l,args with
 
 let kill_some_lams bl (ids,c) =
   let n = List.length bl in
-  let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in
-  if n = n' then ids,c
-  else if n' = 0 then [],ast_lift (-n) c
+  let n' = List.fold_left (fun n b -> if b == Keep then (n+1) else n) 0 bl in
+  if Int.equal n n' then ids,c
+  else if Int.equal n' 0 then [],ast_lift (-n) c
   else begin
     let v = Array.make n None in
     let rec parse_ids i j = function
@@ -1041,10 +1050,10 @@ let case_expunge s e =
   if all lambdas are logical dummy and the target language is strict. *)
 
 let term_expunge s (ids,c) =
-  if s = [] then c
+  if List.is_empty s then c
   else
     let ids,c = kill_some_lams (List.rev s) (ids,c) in
-    if ids = [] && lang () <> Haskell && List.mem (Kill Kother) s then
+    if List.is_empty ids && lang () != Haskell && List.mem (Kill Kother) s then
       MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
@@ -1056,7 +1065,7 @@ let kill_dummy_args ids r t =
   let m = List.length ids in
   let bl = List.rev_map sign_of_id ids in
   let rec found n = function
-    | MLrel r' when r' = r + n -> true
+    | MLrel r' when Int.equal r' (r + n) -> true
     | MLmagic e -> found n e
     | _ -> false
   in
@@ -1133,7 +1142,7 @@ let normalize a =
   let o = optims () in
   let rec norm a =
     let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
-    if a = a' then a else norm a'
+    if Pervasives.(=) a a' then a else norm a' (** FIXME *)
   in norm a
 
 (*S Special treatment of fixpoint for pretty-printing purpose. *)
@@ -1156,7 +1165,7 @@ let optimize_fix a =
   else
     let ids,a' = collect_lams a in
     let n = List.length ids in
-    if n = 0 then a
+    if Int.equal n 0 then a
     else match a' with
       | MLfix(_,[|f|],[|c|]) ->
 	  let new_f = MLapp (MLrel (n+1),eta_args n) in
@@ -1224,7 +1233,7 @@ let rec non_stricts add cand = function
       let cand = if add then 1::cand else cand in
       pop 1 (non_stricts add cand t)
   | MLrel n ->
-      List.filter ((<>) n) cand
+      List.filter (fun m -> not (Int.equal m n)) cand
   | MLapp (t,l)->
       let cand = non_stricts false cand t in
       List.fold_left (non_stricts false) cand l
@@ -1334,6 +1343,6 @@ let inline r t =
   not (to_keep r) (* The user DOES want to keep it *)
   && not (is_inline_custom r)
   && (to_inline r (* The user DOES want to inline it *)
-     || (lang () <> Haskell && not (is_projection r) &&
+     || (lang () != Haskell && not (is_projection r) &&
          (is_recursor r || manual_inline r || inline_test r t)))
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 58186e904..45977b657 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -108,13 +108,13 @@ let ind_iter_references do_term do_cons do_type kn ind =
   let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in
   let packet_iter ip p =
     do_type (IndRef ip);
-    if lang () = Ocaml then
+    if lang () == Ocaml then
       (match ind.ind_equiv with
 	 | Miniml.Equiv kne -> do_type (IndRef (mind_of_kn kne, snd ip));
 	 | _ -> ());
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
-  if lang () = Ocaml then record_iter_references do_term ind.ind_kind;
+  if lang () == Ocaml then record_iter_references do_term ind.ind_kind;
     Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
 
 let decl_iter_references do_term do_cons do_type =
@@ -206,7 +206,7 @@ let is_modular = function
 
 let rec search_structure l m = function
   | [] -> raise Not_found
-  | (lab,d)::_ when lab=l && is_modular d = m -> d
+  | (lab,d)::_ when Label.equal lab l && (is_modular d : bool) == m -> d
   | _::fields -> search_structure l m fields
 
 let get_decl_in_structure r struc =
@@ -217,7 +217,7 @@ let get_decl_in_structure r struc =
     let rec go ll sel = match ll with
       | [] -> assert false
       | l :: ll ->
-	  match search_structure l (ll<>[]) sel with
+	  match search_structure l (not (List.is_empty ll)) sel with
 	    | SEdecl d -> d
 	    | SEmodtype m -> assert false
 	    | SEmodule m ->
@@ -349,7 +349,7 @@ let rec depcheck_se = function
     let se' = depcheck_se se in
     let refs = declared_refs d in
     let refs' = List.filter is_needed refs in
-    if refs' = [] then
+    if List.is_empty refs' then
       (List.iter remove_info_axiom refs;
        List.iter remove_opaque refs;
        se')
@@ -372,14 +372,22 @@ let rec depcheck_struct = function
   | (mp,lse)::struc ->
       let struc' = depcheck_struct struc in
       let lse' = depcheck_se lse in
-      if lse' = [] then struc' else (mp,lse')::struc'
+      if List.is_empty lse' then struc' else (mp,lse')::struc'
+
+let is_prefix pre s =
+  let len = String.length pre in
+  let rec is_prefix_aux i =
+    if Int.equal i len then true
+    else pre.[i] == s.[i] && is_prefix_aux (succ i)
+  in
+  is_prefix_aux 0
 
 let check_implicits = function
   | MLexn s ->
-      if String.length s > 8 && (s.[0] = 'U' || s.[0] = 'I') then
+      if String.length s > 8 && (s.[0] == 'U' || s.[0] == 'I') then
 	begin
-	  if String.sub s 0 7 = "UNBOUND" then assert false;
-	  if String.sub s 0 8 = "IMPLICIT" then
+	  if is_prefix "UNBOUND" s then assert false;
+	  if is_prefix "IMPLICIT" s then
 	    error_non_implicit (String.sub s 9 (String.length s - 9));
 	end;
       false
@@ -393,7 +401,7 @@ let optimize_struct to_appear struc =
   in
   ignore (struct_ast_search check_implicits opt_struc);
   if library () then
-    List.filter (fun (_,lse) -> lse<>[]) opt_struc
+    List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc
   else begin
     reset_needed ();
     List.iter add_needed (fst to_appear);
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index f3d6bcb98..d76235897 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -25,7 +25,7 @@ open Common
 
 let pp_tvar id =
   let s = Id.to_string id in
-  if String.length s < 2 || s.[1]<>'\''
+  if String.length s < 2 || s.[1] != '\''
   then str ("'"^s)
   else str ("' "^s)
 
@@ -36,10 +36,10 @@ let pp_abst = function
       str " ->" ++ spc ()
 
 let pp_parameters l =
-  (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
+  (pp_boxed_tuple pp_tvar l ++ space_if (not (List.is_empty l)))
 
 let pp_string_parameters l =
-  (pp_boxed_tuple str l ++ space_if (l<>[]))
+  (pp_boxed_tuple str l ++ space_if (not (List.is_empty l)))
 
 let pp_letin pat def body =
   let fstline = str "let " ++ pat ++ str " =" ++ spc () ++ def in
@@ -70,7 +70,7 @@ let pp_header_comment = function
 let preamble _ comment used_modules usf =
   pp_header_comment comment ++
   prlist pp_open used_modules ++
-  (if used_modules = [] then mt () else fnl ()) ++
+  (if List.is_empty used_modules then mt () else fnl ()) ++
   (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++
   (if usf.mldummy then
      str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n"
@@ -80,7 +80,7 @@ let preamble _ comment used_modules usf =
 let sig_preamble _ comment used_modules usf =
   pp_header_comment comment ++ fnl () ++ fnl () ++
   prlist pp_open used_modules ++
-  (if used_modules = [] then mt () else fnl ()) ++
+  (if List.is_empty used_modules then mt () else fnl ()) ++
   (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt())
 
 (*s The pretty-printer for Ocaml syntax*)
@@ -101,7 +101,7 @@ let is_infix r =
   is_inline_custom r &&
   (let s = find_custom r in
    let l = String.length s in
-   l >= 2 && s.[0] = '(' && s.[l-1] = ')')
+   l >= 2 && s.[0] == '(' && s.[l-1] == ')')
 
 let get_infix r =
   let s = find_custom r in
@@ -132,7 +132,7 @@ let pp_type par vl t =
 	pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
     | Tglob (r,[]) -> pp_global Type r
     | Tglob (IndRef(kn,0),l)
-	when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->
+	when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
 	pp_tuple_light pp_rec l
     | Tglob (r,l) ->
 	pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
@@ -156,7 +156,7 @@ let is_bool_patt p s =
       | Pcons (r,[]) -> r
       | _ -> raise Not_found
     in
-    find_custom r = s
+    String.equal (find_custom r) s
   with Not_found -> false
 
 
@@ -210,35 +210,35 @@ let rec pp_expr par env args =
     | MLaxiom ->
 	pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
     | MLcons (_,r,a) as c ->
-        assert (args=[]);
+        assert (List.is_empty args);
         begin match a with
 	  | _ when is_native_char c -> pp_native_char c
 	  | [a1;a2] when is_infix r ->
 	    let pp = pp_expr true env [] in
 	    pp_par par (pp a1 ++ str (get_infix r) ++ pp a2)
 	  | _ when is_coinductive r ->
-	    let ne = (a<>[]) in
+	    let ne = not (List.is_empty a) in
 	    let tuple = space_if ne ++ pp_tuple (pp_expr true env []) a in
 	    pp_par par (str "lazy " ++ pp_par ne (pp_global Cons r ++ tuple))
 	  | [] -> pp_global Cons r
 	  | _ ->
 	    let fds = get_record_fields r in
-	    if fds <> [] then
+	    if not (List.is_empty fds) then
 	      pp_record_pat (pp_fields r fds, List.map (pp_expr true env []) a)
 	    else
 	      let tuple = pp_tuple (pp_expr true env []) a in
-	      if str_global Cons r = "" (* hack Extract Inductive prod *)
+	      if String.is_empty (str_global Cons r) (* hack Extract Inductive prod *)
 	      then tuple
 	      else pp_par par (pp_global Cons r ++ spc () ++ tuple)
 	end
     | MLtuple l ->
-        assert (args = []);
+        assert (List.is_empty args);
         pp_boxed_tuple (pp_expr true env []) l
     | MLcase (_, t, pv) when is_custom_match pv ->
         if not (is_regular_match pv) then
 	  error "Cannot mix yet user-given match and general patterns.";
 	let mkfun (ids,_,e) =
-	  if ids <> [] then named_lams (List.rev ids) e
+	  if not (List.is_empty ids) then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
 	in
 	let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in
@@ -257,7 +257,7 @@ let rec pp_expr par env args =
         (try pp_record_proj par env typ t pv args
 	 with Impossible ->
 	   (* Second, can this match be printed as a let-in ? *)
-	   if Array.length pv = 1 then
+	   if Int.equal (Array.length pv) 1 then
 	     let s1,s2 = pp_one_pat env pv.(0) in
 	     hv 0 (apply2 (pp_letin s1 head s2))
 	   else
@@ -272,8 +272,8 @@ let rec pp_expr par env args =
 and pp_record_proj par env typ t pv args =
   (* Can a match be printed as a mere record projection ? *)
   let fields = record_fields_of_type typ in
-  if fields = [] then raise Impossible;
-  if Array.length pv <> 1 then raise Impossible;
+  if List.is_empty fields then raise Impossible;
+  if not (Int.equal (Array.length pv) 1) then raise Impossible;
   if has_deep_pattern pv then raise Impossible;
   let (ids,pat,body) = pv.(0) in
   let n = List.length ids in
@@ -284,7 +284,7 @@ and pp_record_proj par env typ t pv args =
     | _ -> raise Impossible
   in
   let rec lookup_rel i idx = function
-    | Prel j :: l -> if i = j then idx else lookup_rel i (idx+1) l
+    | Prel j :: l -> if Int.equal i j then idx else lookup_rel i (idx+1) l
     | Pwild :: l -> lookup_rel i (idx+1) l
     | _ -> raise Impossible
   in
@@ -308,15 +308,15 @@ and pp_record_pat (fields, args) =
    str " }"
 
 and pp_cons_pat r ppl =
-  if is_infix r && List.length ppl = 2 then
+  if is_infix r && Int.equal (List.length ppl) 2 then
     List.hd ppl ++ str (get_infix r) ++ List.hd (List.tl ppl)
   else
     let fields = get_record_fields r in
-    if fields <> [] then pp_record_pat (pp_fields r fields, ppl)
-    else if str_global Cons r = "" then
+    if not (List.is_empty fields) then pp_record_pat (pp_fields r fields, ppl)
+    else if String.is_empty (str_global Cons r) then
       pp_boxed_tuple identity ppl (* Hack Extract Inductive prod *)
     else
-      pp_global Cons r ++ space_if (ppl<>[]) ++ pp_boxed_tuple identity ppl
+      pp_global Cons r ++ space_if (not (List.is_empty ppl)) ++ pp_boxed_tuple identity ppl
 
 and pp_gen_pat ids env = function
   | Pcons (r, l) -> pp_cons_pat r (List.map (pp_gen_pat ids env) l)
@@ -346,7 +346,7 @@ and pp_pat env pv =
     (fun i x ->
        let s1,s2 = pp_one_pat env x in
        hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++
-       if i = Array.length pv - 1 then mt () else fnl ())
+       if Int.equal i (Array.length pv - 1) then mt () else fnl ())
     pv
 
 and pp_function env t =
@@ -354,7 +354,7 @@ and pp_function env t =
   let bl,env' = push_vars (List.map id_of_mlid bl) env in
   match t' with
     | MLcase(Tglob(r,_),MLrel 1,pv) when
-	not (is_coinductive r) && get_record_fields r = [] &&
+	not (is_coinductive r) && List.is_empty (get_record_fields r) &&
 	not (is_custom_match pv) ->
 	if not (ast_occurs 1 (MLcase(Tunknown,MLdummy,pv))) then
 	  pr_binding (List.rev (List.tl bl)) ++
@@ -397,7 +397,7 @@ let pp_Dfix (rv,c,t) =
       (if init then failwith "empty phrase" else mt ())
     else
       let void = is_inline_custom rv.(i) ||
-	(not (is_custom rv.(i)) && c.(i) = MLexn "UNUSED")
+	(not (is_custom rv.(i)) && match c.(i) with MLexn "UNUSED" -> true | _ -> false)
       in
       if void then pp init (i+1)
       else
@@ -424,15 +424,15 @@ let pp_equiv param_list name = function
 let pp_one_ind prefix ip_equiv pl name cnames ctyps =
   let pl = rename_tvars keywords pl in
   let pp_constructor i typs =
-    (if i=0 then mt () else fnl ()) ++
+    (if Int.equal i 0 then mt () else fnl ()) ++
     hov 3 (str "| " ++ cnames.(i) ++
-	   (if typs = [] then mt () else str " of ") ++
+	   (if List.is_empty typs then mt () else str " of ") ++
 	   prlist_with_sep
 	    (fun () -> spc () ++ str "* ") (pp_type true pl) typs)
   in
   pp_parameters pl ++ str prefix ++ name ++
   pp_equiv pl name ip_equiv ++ str " =" ++
-  if Array.length ctyps = 0 then str " unit (* empty inductive *)"
+  if Int.equal (Array.length ctyps) 0 then str " unit (* empty inductive *)"
   else fnl () ++ v 0 (prvecti pp_constructor ctyps)
 
 let pp_logical_ind packet =
@@ -531,7 +531,7 @@ let pp_decl = function
 	    pp_string_parameters ids, str "=" ++ spc () ++ str s
 	  with Not_found ->
 	    pp_parameters l,
-	    if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
+	    if t == Taxiom then str "(* AXIOM TO BE REALIZED *)"
 	    else str "=" ++ spc () ++ pp_type false l t
 	in
 	hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
@@ -678,7 +678,7 @@ let rec pp_structure_elem = function
   | (l,SEmodule m) ->
       let typ =
         (* virtual printing of the type, in order to have a correct mli later*)
-	if Common.get_phase () = Pre then
+	if Common.get_phase () == Pre then
 	  str ": " ++ pp_module_type [] m.ml_mod_type
 	else mt ()
       in
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 8125b4757..b7c67588d 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -42,7 +42,7 @@ let preamble _ comment _ usf =
 let pr_id id =
   let s = Id.to_string id in
   for i = 0 to String.length s - 1 do
-    if s.[i] = '\'' then s.[i] <- '~'
+    if s.[i] == '\'' then s.[i] <- '~'
   done;
   str s
 
@@ -92,11 +92,11 @@ let rec pp_expr env args =
     | MLglob r ->
 	apply (pp_global Term r)
     | MLcons (_,r,args') ->
-	assert (args=[]);
+	assert (List.is_empty args);
 	let st =
 	  str "`" ++
 	  paren (pp_global Cons r ++
-		 (if args' = [] then mt () else spc ()) ++
+		 (if List.is_empty args' then mt () else spc ()) ++
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in
 	if is_coinductive r then paren (str "delay " ++ st) else st
@@ -105,7 +105,7 @@ let rec pp_expr env args =
 	error "Cannot handle general patterns in Scheme yet."
     | MLcase (_,t,pv) when is_custom_match pv ->
 	let mkfun (ids,_,e) =
-	  if ids <> [] then named_lams (List.rev ids) e
+	  if not (List.is_empty ids) then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
 	in
 	apply
@@ -135,7 +135,7 @@ let rec pp_expr env args =
 and pp_cons_args env = function
   | MLcons (_,r,args) when is_coinductive r ->
       paren (pp_global Cons r ++
-	     (if args = [] then mt () else spc ()) ++
+	     (if List.is_empty args then mt () else spc ()) ++
 	     prlist_with_sep spc (pp_cons_args env) args)
   | e -> str "," ++ pp_expr env [] e
 
@@ -147,7 +147,7 @@ and pp_one_pat env (ids,p,t) =
   in
   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
   let args =
-    if ids = [] then mt ()
+    if List.is_empty ids then mt ()
     else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
   in
   (pp_global Cons r ++ args), (pp_expr env' [] t)
@@ -183,7 +183,7 @@ let pp_decl = function
       prvecti
 	(fun i r ->
 	  let void = is_inline_custom r ||
-	    (not (is_custom r) && defs.(i) = MLexn "UNUSED")
+	    (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
 	  in
 	  if void then mt ()
 	  else
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 66acf23ed..4e60696a8 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -79,7 +79,7 @@ let rec prefixes_mp mp = match mp with
   | _ -> MPset.singleton mp
 
 let rec get_nth_label_mp n = function
-  | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp
+  | MPdot (mp,l) -> if Int.equal n 1 then l else get_nth_label_mp (n-1) mp
   | _ -> failwith "get_nth_label: not enough MPdot"
 
 let common_prefix_from_list mp0 mpl =
@@ -90,7 +90,7 @@ let common_prefix_from_list mp0 mpl =
   in f mpl
 
 let rec parse_labels2 ll mp1 = function
-  | mp when mp1=mp -> mp,ll
+  | mp when ModPath.equal mp1 mp -> mp,ll
   | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp
   | mp -> mp,ll
 
@@ -137,7 +137,7 @@ let is_coinductive r =
     | IndRef (kn,_) -> kn
     | _ -> assert false
   in
-  try Mindmap_env.find kn !inductive_kinds = Coinductive
+  try Mindmap_env.find kn !inductive_kinds == Coinductive
   with Not_found -> false
 
 let is_coinductive_type = function
@@ -278,18 +278,18 @@ let err s = errorlabstrm "Extraction" s
 
 let warning_axioms () =
   let info_axioms = Refset'.elements !info_axioms in
-  if info_axioms = [] then ()
+  if List.is_empty info_axioms then ()
   else begin
-    let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
+    let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in
     msg_warning
       (str ("The following "^s^" must be realized in the extracted code:")
        ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
        ++ str "." ++ fnl ())
   end;
   let log_axioms = Refset'.elements !log_axioms in
-  if log_axioms = [] then ()
+  if List.is_empty log_axioms then ()
   else begin
-    let s = if List.length log_axioms = 1 then "axiom was" else "axioms were"
+    let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were"
     in
     msg_warning
       (str ("The following logical "^s^" encountered:") ++
@@ -300,13 +300,13 @@ let warning_axioms () =
        spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
        fnl ())
   end;
-  if !Flags.load_proofs = Flags.Dont && info_axioms@log_axioms <> [] then
+  if !Flags.load_proofs == Flags.Dont && not (List.is_empty (info_axioms@log_axioms)) then
     msg_warning
       (str "Some of these axioms might be due to option -dont-load-proofs.")
 
 let warning_opaques accessed =
   let opaques = Refset'.elements !opaques in
-  if opaques = [] then ()
+  if List.is_empty opaques then ()
   else
     let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
     if accessed then
@@ -478,7 +478,7 @@ type opt_flag =
       opt_lin_let : bool;   (* 512 *)
       opt_lin_beta : bool } (* 1024 *)
 
-let kth_digit n k = (n land (1 lsl k) <> 0)
+let kth_digit n k = not (Int.equal (n land (1 lsl k)) 0)
 
 let flag_of_int n =
     { opt_kill_dum = kth_digit n 0;
@@ -515,7 +515,7 @@ let _ = declare_bool_option
            optdepr = false;
 	   optname = "Extraction Optimize";
 	   optkey = ["Extraction"; "Optimize"];
-	   optread = (fun () -> !int_flag_ref <> 0);
+	   optread = (fun () -> not (Int.equal !int_flag_ref 0));
 	   optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
 
 let _ = declare_int_option
@@ -711,7 +711,7 @@ let file_of_modfile mp =
     | _ -> assert false
   in
   let s = String.copy (string_of_modfile mp) in
-  if s.[0] <> s0.[0] then s.[0] <- s0.[0];
+  if s.[0] != s0.[0] then s.[0] <- s0.[0];
   s
 
 let add_blacklist_entries l =
@@ -773,7 +773,7 @@ let add_custom_match r s =
   custom_matchs := Refmap'.add r s !custom_matchs
 
 let indref_of_match pv =
-  if Array.length pv = 0 then raise Not_found;
+  if Array.is_empty pv then raise Not_found;
   let (_,pat,_) = pv.(0) in
   match pat with
     | Pusual (ConstructRef (ip,_)) -> IndRef ip
@@ -821,7 +821,7 @@ let extract_constant_inline inline r ids s =
 	if Reduction.is_arity env typ
 	  then begin
 	    let nargs = Hook.get use_type_scheme_nb_args env typ in
-	    if List.length ids <> nargs then error_axiom_scheme g nargs
+	    if not (Int.equal (List.length ids) nargs) then error_axiom_scheme g nargs
 	  end;
 	Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
 	Lib.add_anonymous_leaf (in_customs (g,ids,s))
@@ -836,7 +836,7 @@ let extract_inductive r s l optstr =
     | IndRef ((kn,i) as ip) ->
 	let mib = Global.lookup_mind kn in
 	let n = Array.length mib.mind_packets.(i).mind_consnames in
-	if n <> List.length l then error_nb_cons ();
+	if not (Int.equal n (List.length l)) then error_nb_cons ();
 	Lib.add_anonymous_leaf (inline_extraction (true,[g]));
 	Lib.add_anonymous_leaf (in_customs (g,[],s));
 	Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))