Removing a bunch of generic equalities.

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

38 files changed, 512 insertions, 473 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 11786cbdc..c067b1c00 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -103,6 +103,12 @@ type cinfo=
      ci_arity: int;     (* # args *)
      ci_nhyps: int}     (* # projectable args *)
 
+let family_eq f1 f2 = match f1, f2 with
+| InProp, InProp
+| InSet, InSet
+| InType, InType -> true
+| _ -> false
+
 type term=
     Symb of constr
   | Product of sorts_family * sorts_family
@@ -113,13 +119,13 @@ type term=
 let rec term_equal t1 t2 =
   match t1, t2 with
     | Symb c1, Symb c2 -> eq_constr c1 c2
-    | Product (s1, t1), Product (s2, t2) -> s1 = s2 && t1 = t2
-    | Eps i1, Eps i2 -> Id.compare i1 i2 = 0
+    | Product (s1, t1), Product (s2, t2) -> family_eq s1 s2 && family_eq t1 t2
+    | Eps i1, Eps i2 -> Id.equal i1 i2
     | Appli (t1, u1), Appli (t2, u2) -> term_equal t1 t2 && term_equal u1 u2
     | Constructor {ci_constr=c1; ci_arity=i1; ci_nhyps=j1},
       Constructor {ci_constr=c2; ci_arity=i2; ci_nhyps=j2} ->
-      i1 = i2 && j1 = j2 && eq_constructor c1 c2
-    | _ -> t1 = t2
+      Int.equal i1 i2 && Int.equal j1 j2 && eq_constructor c1 c2
+    | _ -> false
 
 open Hashset.Combine
 
@@ -341,7 +347,7 @@ let signature uf i=
 let next uf=
   let size=uf.size in
   let nsize= succ size in
-    if nsize=uf.max_size then
+    if Int.equal nsize uf.max_size then
       let newmax=uf.max_size * 3 / 2 + 1 in
       let newmap=Array.make newmax dummy_node in
 	begin
@@ -512,7 +518,7 @@ let is_redundant state id args =
     let prev_args = Identhash.find_all state.q_history id in
     List.exists
       (fun old_args ->
-	 Util.Array.for_all2 (fun i j -> i = find state.uf j)
+	 Util.Array.for_all2 (fun i j -> Int.equal i (find state.uf j))
          norm_args old_args)
       prev_args
     with Not_found -> false
@@ -562,14 +568,16 @@ let rec down_path uf i l=
       Eqto(j,t)->down_path uf j (((i,j),t)::l)
     | Rep _ ->l
 
+let eq_pair (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2
+
 let rec min_path=function
     ([],l2)->([],l2)
   | (l1,[])->(l1,[])
-  | (((c1,t1)::q1),((c2,t2)::q2)) when c1=c2 -> min_path (q1,q2)
+  | (((c1,t1)::q1),((c2,t2)::q2)) when eq_pair c1 c2 -> min_path (q1,q2)
   | cpl -> cpl
 
 let join_path uf i j=
-  assert (find uf i=find uf j);
+  assert (Int.equal (find uf i) (find uf j));
   min_path (down_path uf i [],down_path uf j [])
 
 let union state i1 i2 eq=
@@ -619,7 +627,7 @@ let merge eq state = (* merge and no-merge *)
   let uf=state.uf in
   let i=find uf eq.lhs
   and j=find uf eq.rhs in
-    if i<>j then
+    if not (Int.equal i j) then
       if (size uf i)<(size uf j) then
 	union state i j eq
       else
@@ -657,7 +665,7 @@ let process_function_mark t rep paf state  =
 let process_constructor_mark t i rep pac state =
     match rep.inductive_status with
 	Total (s,opac) ->
-	  if pac.cnode <> opac.cnode then (* Conflict *)
+	  if not (Int.equal pac.cnode opac.cnode) then (* Conflict *)
 	    raise (Discriminable (s,opac,t,pac))
 	  else (* Match *)
 	    let cinfo = get_constructor_info state.uf pac.cnode in
@@ -676,7 +684,7 @@ let process_constructor_mark t i rep pac state =
 	  add_pac rep pac t;
 	  state.terms<-Int.Set.union rep.lfathers state.terms
       | Unknown ->
-	  if pac.arity = 0 then
+	  if Int.equal pac.arity 0 then
 	    rep.inductive_status <- Total (t,pac)
 	  else
 	    begin
@@ -705,7 +713,7 @@ let check_disequalities state =
   let rec check_aux = function
     | dis::q ->
         let (info, ans) =
-          if find uf dis.lhs = find uf dis.rhs then (str "Yes", Some dis)
+          if Int.equal (find uf dis.lhs) (find uf dis.rhs) then (str "Yes", Some dis)
           else (str "No", check_aux q)
         in
         let _ = debug
@@ -803,13 +811,13 @@ let do_match state res pb_stack =
 		      Stack.push {mp with mp_stack=remains} pb_stack
 		    end
 		  else
-		    if mp.mp_subst.(pred i) = cl then
+		    if Int.equal mp.mp_subst.(pred i) cl then
 		      Stack.push {mp with mp_stack=remains} pb_stack
 		    else (* mismatch for non-linear variable in pattern *) ()
 	      | PApp (f,[]) ->
 		  begin
 		    try let j=Termhash.find uf.syms f in
-		      if find uf j =cl then
+		      if Int.equal (find uf j) cl then
 			Stack.push {mp with mp_stack=remains} pb_stack
 		    with Not_found -> ()
 		  end
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 780a4877a..6c578f1c2 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -90,7 +90,7 @@ let atom_of_constr env sigma term =
   let kot = kind_of_term wh in
     match kot with
       App (f,args)->
-	  if eq_constr f (Lazy.force _eq) && (Array.length args)=3
+	  if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
 	  then `Eq (args.(0),
 		   decompose_term env sigma args.(1),
 		   decompose_term env sigma args.(2))
@@ -125,20 +125,20 @@ let non_trivial = function
 let patterns_of_constr env sigma nrels term=
   let f,args=
     try destApp (whd_delta env term) with DestKO -> raise Not_found in
-	if eq_constr f (Lazy.force _eq) && (Array.length args)=3
+	if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
 	then
 	  let patt1,rels1 = pattern_of_constr env sigma args.(1)
 	  and patt2,rels2 = pattern_of_constr env sigma args.(2) in
 	  let valid1 =
-	    if Int.Set.cardinal rels1 <> nrels then Creates_variables
+	    if not (Int.equal (Int.Set.cardinal rels1) nrels) then Creates_variables
 	    else if non_trivial patt1 then Normal
 	    else Trivial args.(0)
 	  and valid2 =
-	    if Int.Set.cardinal rels2 <> nrels then Creates_variables
+	    if not (Int.equal (Int.Set.cardinal rels2) nrels) then Creates_variables
 	    else if non_trivial patt2 then Normal
 	    else Trivial args.(0) in
-	    if valid1 <> Creates_variables
-	      || valid2 <> Creates_variables  then
+	    if valid1 != Creates_variables
+	      || valid2 != Creates_variables  then
 	      nrels,valid1,patt1,valid2,patt2
 	    else raise Not_found
 	else raise Not_found
@@ -230,7 +230,7 @@ let build_projection intype outtype (cstr:constructor) special default gls=
     let ti= prod_appvect types.(i) argv in
     let rc=fst (decompose_prod_assum ti) in
     let head=
-      if i=ci then special else default in
+      if Int.equal i ci then special else default in
       it_mkLambda_or_LetIn head rc in
   let branches=Array.init lp branch in
   let casee=mkRel 1 in
@@ -453,7 +453,7 @@ let f_equal gl =
   try match kind_of_term (pf_concl gl) with
     | App (r,[|_;t;t'|]) when eq_constr r (Lazy.force _eq) ->
 	begin match kind_of_term t, kind_of_term t' with
-	  | App (f,v), App (f',v') when Array.length v = Array.length v' ->
+	  | App (f,v), App (f',v') when Int.equal (Array.length v) (Array.length v') ->
 	      let rec cuts i =
 		if i < 0 then tclTRY (congruence_tac 1000 [])
 		else tclTHENFIRST (cut_eq v.(i) v'.(i)) (cuts (i-1))
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 52fb935d4..8060dcabf 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -24,7 +24,7 @@ open Misctypes
 
 (* INTERN *)
 
-let glob_app (loc,hd,args) = if args =[] then hd else GApp(loc,hd,args)
+let glob_app (loc,hd,args) = if List.is_empty args then hd else GApp(loc,hd,args)
 
 let intern_justification_items globs =
   Option.map (List.map (intern_constr globs))
@@ -164,7 +164,7 @@ let decompose_eq env id =
   let whd = special_whd env typ in
     match kind_of_term whd with
 	App (f,args)->
-	  if eq_constr f _eq && (Array.length args)=3
+	  if eq_constr f _eq && Int.equal (Array.length args) 3
 	  then args.(0)
 	  else error "Previous step is not an equality."
       | _ -> error "Previous step is not an equality."
@@ -328,10 +328,10 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let num_params = pinfo.per_nparams in
   let _ =
     let expected = mib.Declarations.mind_nparams - num_params in
-      if List.length params <> expected then
+      if not (Int.equal (List.length params) expected) then
 	errorlabstrm "suppose it is" 
 	  (str "Wrong number of extra arguments: " ++ 
-	     (if expected = 0 then str "none" else int expected) ++ spc () ++
+	     (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
 	     str "expected.") in
   let app_ind =
     let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind) in
diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml
index 0cbd26316..f3c5da2ad 100644
--- a/plugins/decl_mode/decl_mode.ml
+++ b/plugins/decl_mode/decl_mode.ml
@@ -77,8 +77,9 @@ let get_current_mode () =
   with Proof_global.NoCurrentProof -> Mode_none
 
 let check_not_proof_mode str =
- if get_current_mode () = Mode_proof then
-   error str
+ match get_current_mode () with
+ | Mode_proof -> error str
+ | _ -> ()
 
 let get_info sigma gl=
   match Store.get (Goal.V82.extra sigma gl) info with
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index e3ef0671c..cca17a17e 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -77,7 +77,7 @@ let special_nf gl=
 
 let is_good_inductive env ind =
   let mib,oib = Inductive.lookup_mind_specif env ind in
-    oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib))
+    Int.equal oib.mind_nrealargs 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib))
 
 let check_not_per pts =
   if not (Proof.is_done pts) then
@@ -93,7 +93,7 @@ let mk_evd metalist gls =
     meta_declare meta typ evd in
     List.fold_right add_one metalist evd0
 
-let is_tmp id = (Id.to_string id).[0] = '_'
+let is_tmp id = (Id.to_string id).[0] == '_'
 
 let tmp_ids gls =
   let ctx = pf_hyps gls in
@@ -289,7 +289,7 @@ type stackd_elt =
 
 let rec replace_in_list m l = function
     [] -> raise Not_found
-  | c::q -> if m=fst c then l@q else c::replace_in_list m l q
+  | c::q -> if Int.equal m (fst c) then l@q else c::replace_in_list m l q
 
 let enstack_subsubgoals env se stack gls=
   let hd,params = decompose_app (special_whd gls se.se_type) in
@@ -390,7 +390,7 @@ let concl_refiner metas body gls =
 	let nenv = Environ.push_named (_x,None,_A) env in
 	let asort = family_of_sort (Typing.sort_of nenv evd _A) in
 	let nsubst = (n,mkVar _x)::subst in
-	  if rest = [] then
+	  if List.is_empty rest then
 	    asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
 	  else
 	    let bsort,_B,nbody =
@@ -438,7 +438,7 @@ let thus_tac c ctyp submetas gls =
       find_subsubgoal c ctyp 0 submetas gls
     with Not_found ->
       error "I could not relate this statement to the thesis." in
-  if list = [] then
+  if List.is_empty list then
     exact_check proof gls
   else
     let refiner = concl_refiner list proof gls in
@@ -498,7 +498,7 @@ let decompose_eq id gls =
   let whd =  (special_whd gls typ) in
     match kind_of_term whd with
 	App (f,args)->
-	  if eq_constr f _eq && (Array.length args)=3
+	  if eq_constr f _eq && Int.equal (Array.length args) 3
 	  then (args.(0),
 		args.(1),
 		args.(2))
@@ -672,7 +672,7 @@ let conjunction_arity id gls =
 	    Inductive.lookup_mind_specif env ind in
           let gentypes=
             Inductive.arities_of_constructors ind (mib,oib) in
-	  let _ = if Array.length gentypes <> 1 then raise Not_found in
+	  let _ = if not (Int.equal (Array.length gentypes) 1) then raise Not_found in
 	  let apptype = prod_applist gentypes.(0) params in
 	  let rc,_ = Reduction.dest_prod env apptype in
 	    List.length rc
@@ -791,7 +791,7 @@ let is_rec_pos (main_ind,wft) =
       None -> false
     | Some index ->
 	match fst (Rtree.dest_node wft) with
-	    Mrec (_,i) when i = index -> true
+	    Mrec (_,i) when Int.equal i index -> true
 	  | _ -> false
 
 let rec constr_trees (main_ind,wft) ind =
@@ -876,7 +876,7 @@ let per_tac etype casee gls=
 	      {pm_stack=
 		  Per(etype,per_info,ek,[])::info.pm_stack} gls
       | Virtual cut ->
-	  assert (cut.cut_stat.st_label=Anonymous);
+	  assert (cut.cut_stat.st_label == Anonymous);
 	  let id = pf_get_new_id (Id.of_string "anonymous_matched") gls in
 	  let c = mkVar id in
 	  let modified_cut =
@@ -940,7 +940,7 @@ let rec tree_of_pats ((id,_) as cpl) pats =
 			       tree_of_pats cpl (rest_args::stack))
 		| PatCstr (_,(ind,cnum),args,nam) ->
 		    let nexti i ati =
-		      if i = pred cnum then
+		      if Int.equal i (pred cnum) then
 			let nargs =
 			  List.map_i (fun j a -> (a,ati.(j))) 0 args in
 			  Some (Id.Set.singleton id,
@@ -985,7 +985,7 @@ let rec add_branch ((id,_) as cpl) pats tree=
 		      match tree with
 			Skip_patt (ids,t) ->
 			  let nexti i ati =
-			    if i = pred cnum then
+			    if Int.equal i (pred cnum) then
 			      let nargs =
 				List.map_i (fun j a -> (a,ati.(j))) 0 args in
 				Some (Id.Set.add id ids,
@@ -996,11 +996,11 @@ let rec add_branch ((id,_) as cpl) pats tree=
 				    skip_args t ids (Array.length ati))
 			  in init_tree ids ind rp nexti
 		      | Split_patt (_,ind0,_) ->
-			  if (ind <> ind0) then error
+			  if (not (eq_ind ind ind0)) then error
 			    (* this can happen with coercions *)
 	                    "Case pattern belongs to wrong inductive type.";
 			  let mapi i ati bri =
-			    if i = pred cnum then
+			    if Int.equal i (pred cnum) then
 			      let nargs =
 				List.map_i (fun j a -> (a,ati.(j))) 0 args in
 				append_branch cpl 0
@@ -1029,14 +1029,14 @@ and append_tree ((id,_) as cpl) depth pats tree =
 
 let rec st_assoc id = function
     [] -> raise Not_found
-  | st::_ when st.st_label = id  -> st.st_it
+  | st::_ when Name.equal st.st_label id  -> st.st_it
   | _ :: rest -> st_assoc id rest
 
 let thesis_for obj typ per_info env=
   let rc,hd1=decompose_prod typ in
   let cind,all_args=decompose_app typ in
   let ind = destInd cind in
-  let _ = if ind <> per_info.per_ind then
+  let _ = if not (eq_ind ind per_info.per_ind) then
     errorlabstrm "thesis_for"
       ((Printer.pr_constr_env env obj) ++ spc () ++
 	 str"cannot give an induction hypothesis (wrong inductive type).") in
@@ -1170,7 +1170,7 @@ let hrec_for fix_id per_info gls obj_id =
   let typ=pf_get_hyp_typ gls obj_id in
   let rc,hd1=decompose_prod typ in
   let cind,all_args=decompose_app typ in
-  let ind = destInd cind in assert (ind=per_info.per_ind);
+  let ind = destInd cind in assert (eq_ind ind per_info.per_ind);
   let params,args= List.chop per_info.per_nparams all_args in
   assert begin
     try List.for_all2 eq_constr params per_info.per_params with
@@ -1209,7 +1209,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	let env=pf_env gls in
 	let ctyp=pf_type_of gls casee in
 	let hd,all_args = decompose_app (special_whd gls ctyp) in
-	let _ = assert (destInd hd = ind) in (* just in case *)
+	let _ = assert (eq_ind (destInd hd) ind) in (* just in case *)
 	let params,real_args = List.chop nparams all_args in
 	let abstract_obj c body =
 	  let typ=pf_type_of gls c in
@@ -1230,7 +1230,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 	  let args_ids = constr_args_ids.(i) in
 	  let rec aux n = function
 	      [] ->
-		assert (n=Array.length recargs);
+		assert (Int.equal n (Array.length recargs));
 		next_objs,[],nhrec
 	    | id :: q ->
 		let objs,recs,nrec = aux (succ n) q in
@@ -1302,14 +1302,12 @@ let end_tac et2 gls =
       | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses)
       | [] ->
 	  anomaly (Pp.str "This case should already be trapped") in
-  let et =
-    if et1 <> et2 then
-      match et1 with
-	  ET_Case_analysis ->
-	    error "\"end cases\" expected."
-	| ET_Induction ->
-	    error "\"end induction\" expected."
-    else et1 in
+  let et = match et1, et2 with
+  | ET_Case_analysis, ET_Case_analysis -> et1
+  | ET_Induction, ET_Induction -> et1
+  | ET_Case_analysis, _ -> error "\"end cases\" expected."
+  | ET_Induction, _ -> error "\"end induction\" expected."
+  in
     tclTHEN
       tcl_erase_info
       begin
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)))
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 89ba7b259..03a832e90 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -22,11 +22,11 @@ let red_flags=ref Closure.betaiotazeta
 
 let (=?) f g i1 i2 j1 j2=
   let c=f i1 i2 in
-    if c=0 then g j1 j2 else c
+    if Int.equal c 0 then g j1 j2 else c
 
 let (==?) fg h i1 i2 j1 j2 k1 k2=
   let c=fg i1 i2 j1 j2 in
-    if c=0 then h k1 k2 else c
+    if Int.equal c 0 then h k1 k2 else c
 
 type ('a,'b) sum = Left of 'a | Right of 'b
 
@@ -88,20 +88,20 @@ let kind_of_formula gl term =
 		    let ind=destInd i in
 		    let (mib,mip) = Global.lookup_inductive ind in
 		    let nconstr=Array.length mip.mind_consnames in
-		      if nconstr=0 then
+		      if Int.equal nconstr 0 then
 			False(ind,l)
 		      else
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    nb_prod c = mib.mind_nparams in
+			    Int.equal (nb_prod c) mib.mind_nparams in
 			    Array.exists is_constant mip.mind_nf_lc in
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
 			  then
 			    Atom cciterm
 			  else
-			    if nconstr=1 then
+			    if Int.equal nconstr 1 then
 			      And(ind,l,is_trivial)
 			    else
 			      Or(ind,l,is_trivial)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 4b15dcae5..ac612d0cd 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -30,8 +30,8 @@ let compare_instance inst1 inst2=
 	      (OrderedConstr.compare d1 d2)
 	  | Real((m1,c1),n1),Real((m2,c2),n2)->
 	      ((-) =? (-) ==? OrderedConstr.compare) m2 m1 n1 n2 c1 c2
-	  | Phantom(_),Real((m,_),_)-> if m=0 then -1 else 1
-	  | Real((m,_),_),Phantom(_)-> if m=0 then 1 else -1
+	  | Phantom(_),Real((m,_),_)-> if Int.equal m 0 then -1 else 1
+	  | Real((m,_),_),Phantom(_)-> if Int.equal m 0 then 1 else -1
 
 let compare_gr id1 id2 =
   if id1==id2 then 0 else
@@ -115,13 +115,13 @@ let mk_open_instance id gl m t=
 	  | Anonymous ->  dummy_bvid in
   let revt=substl (List.init m (fun i->mkRel (m-i))) t in
   let rec aux n avoid=
-    if n=0 then [] else
+    if Int.equal n 0 then [] else
       let nid=(fresh_id avoid var_id gl) in
 	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
   let nt=it_mkLambda_or_LetIn revt (aux m []) in
   let rawt=Detyping.detype false [] [] nt in
   let rec raux n t=
-    if n=0 then t else
+    if Int.equal n 0 then t else
       match t with
 	  GLambda(loc,name,k,_,t0)->
 	    let t1=raux (n-1) t0 in
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 4e4a6f19f..8b831d595 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -88,7 +88,7 @@ let cm_add typ nam cm=
 let cm_remove typ nam cm=
   try
     let l=CM.find typ cm in
-    let l0=List.filter (fun id->id<>nam) l in
+    let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
       match l0 with
 	  []->CM.remove typ cm
 	| _ ->CM.add typ l0 cm
@@ -118,7 +118,7 @@ let lookup item seq=
 	let p (id2,o)=
 	  match o with
 	      None -> false
-	    | Some ((m2,t2) as c2)->id=id2 && m2>m && more_general c2 c in
+	    | Some ((m2,t2) as c2)-> Globnames.eq_gr id id2 && m2>m && more_general c2 c in
 	  History.exists p seq.history
 
 let add_formula side nam t seq gl=
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index e59f0419e..eeaf270c3 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -42,7 +42,7 @@ let unif t1 t2=
       and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
 	match (kind_of_term nt1),(kind_of_term nt2) with
 	    Meta i,Meta j->
-	      if i<>j then
+	      if not (Int.equal i j) then
 		if i<j then bind j nt1
 		else bind i nt2
 	  | Meta i,_ ->
@@ -63,7 +63,7 @@ let unif t1 t2=
 	      Queue.add (pa,pb) bige;
 	      Queue.add (ca,cb) bige;
 	      let l=Array.length va in
-		if l<>(Array.length vb) then
+		if not (Int.equal l (Array.length vb)) then
 		  raise (UFAIL (nt1,nt2))
 		else
 		  for i=0 to l-1 do
@@ -72,7 +72,7 @@ let unif t1 t2=
 	  | App(ha,va),App(hb,vb)->
 	      Queue.add (ha,hb) bige;
 	      let l=Array.length va in
-		if l<>(Array.length vb) then
+		if not (Int.equal l (Array.length vb)) then
 		  raise (UFAIL (nt1,nt2))
 		else
 		  for i=0 to l-1 do
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 356853573..d249df578 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -306,7 +306,7 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
 	(fun i (end_of_type,ctxt_size,witness_fun) ((x',b',t') as decl) ->
 	   try
 	     let witness = Int.Map.find i sub in
-	     if b' <> None then anomaly (Pp.str "can not redefine a rel!");
+	     if not (Option.is_empty b') then anomaly (Pp.str "can not redefine a rel!");
 	     (Termops.pop end_of_type,ctxt_size,mkLetIn(x',witness,t',witness_fun))
 	   with Not_found  ->
 	     (mkProd_or_LetIn decl end_of_type, ctxt_size + 1, mkLambda_or_LetIn decl witness_fun)
@@ -655,7 +655,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 	)
       )
   in
-  if args_id = []
+  if List.is_empty args_id
   then
     tclTHENLIST [
       tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps;
@@ -1196,7 +1196,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		(fun fi -> fi.name,fi.idx + 1 ,fi.types)
 		(pre_info@others_infos)
 	    in
-	    if other_fix_infos = []
+	    if List.is_empty other_fix_infos
 	    then
 	      (* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
 	    else
@@ -1588,7 +1588,7 @@ let prove_principle_for_gen
 	  (fun g ->
 	     let new_hyps = pf_ids_of_hyps g in
 	     tcc_list := List.rev (List.subtract new_hyps (hid::hyps));
-	     if !tcc_list = []
+	     if List.is_empty !tcc_list
 	     then
 	       begin
 		 tcc_list := [hid];
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index a01039eb0..d11e810e1 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -107,8 +107,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let pre_princ = substl (List.map mkVar ptes_vars) pre_princ in
   let is_dom c =
     match kind_of_term c with
-      | Ind((u,_)) -> u = rel_as_kn
-      | Construct((u,_),_) -> u = rel_as_kn
+      | Ind((u,_)) -> MutInd.equal u rel_as_kn
+      | Construct((u,_),_) -> MutInd.equal u rel_as_kn
       | _ -> false
   in
   let get_fun_num c =
@@ -330,7 +330,7 @@ let generate_functional_principle
   in
   let names = ref [new_princ_name] in
   let hook new_principle_type = Some (fun _ _ ->
-    if sorts = None
+    if Option.is_empty sorts
     then
       (*     let id_of_f = Label.to_id (con_label f) in *)
       let register_with_sort fam_sort =
@@ -375,7 +375,7 @@ let generate_functional_principle
 	  let s = Id.to_string id in
 	  let n = String.length "___________princ_________" in
 	  if String.length s >= n
-	  then if String.sub s 0 n = "___________princ_________"
+	  then if String.equal (String.sub s 0 n) "___________princ_________"
 	  then Pfedit.delete_current_proof ()
 	  else ()
 	  else ()
@@ -430,7 +430,7 @@ let get_funs_constant mp dp =
       let first_params = List.hd l_params  in
       List.iter
 	(fun params ->
-	   if not (List.equal (fun (n1, c1) (n2, c2) -> n1 = n2 && eq_constr c1 c2) first_params params)
+	   if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params)
 	   then error "Not a mutal recursive block"
 	)
 	l_params
@@ -442,14 +442,15 @@ let get_funs_constant mp dp =
 	  match kind_of_term body with
 	    | Fix((idxs,_),(na,ta,ca)) -> (idxs,na,ta,ca)
 	    | _ ->
-		if is_first && (List.length l_bodies = 1)
+		if is_first && Int.equal (List.length l_bodies) 1
 		then raise Not_Rec
 		else error "Not a mutal recursive block"
 	in
 	let first_infos = extract_info true (List.hd l_bodies) in
 	let check body  = (* Hope this is correct *)
 	  let eq_infos (ia1, na1, ta1, ca1) (ia2, na2, ta2, ca2) =
-	    ia1 = ia2 && na1 = na2 && Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2
+            Array.equal Int.equal ia1 ia2 && Array.equal Name.equal na1 na2 &&
+            Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2
 	  in
 	  if not (eq_infos first_infos (extract_info false body))
 	  then  error "Not a mutal recursive block"
@@ -527,7 +528,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
 	  let s = Id.to_string id in
 	  let n = String.length "___________princ_________" in
 	  if String.length s >= n
-	  then if String.sub s 0 n = "___________princ_________"
+	  then if String.equal (String.sub s 0 n) "___________princ_________"
 	  then Pfedit.delete_current_proof ()
 	  else ()
 	  else ()
@@ -548,7 +549,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
   in
   let const = {const with const_entry_opaque = opacity } in
   (* The others are just deduced *)
-  if other_princ_types = []
+  if List.is_empty other_princ_types
   then
     [const]
   else
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 7e229fbd2..cb9d12c5e 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -283,7 +283,7 @@ let constr_head_match u t=
   if isApp u
   then
     let uhd,args= destApp u in
-    uhd=t
+    Constr.equal uhd t
   else false
 
 (** [hdMatchSub inu t] returns the list of occurrences of [t] in
@@ -387,7 +387,7 @@ let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list)
   let info_list = find_fapp test g in
   let ordered_info_list = heuristic info_list in
   prlistconstr (List.map (fun x -> applist (x.fname,x.largs)) ordered_info_list);
-  if List.length ordered_info_list = 0 then Errors.error "function not found in goal\n";
+  if List.is_empty ordered_info_list then Errors.error "function not found in goal\n";
   let taclist: Proof_type.tactic list =
     List.map
       (fun info ->
@@ -476,10 +476,10 @@ VERNAC COMMAND EXTEND MergeFunind CLASSIFIED AS SIDEFF
        let ar1 = List.length (fst (decompose_prod f1type)) in
        let ar2 = List.length (fst (decompose_prod f2type)) in
        let _ =
-	 if ar1 <> List.length cl1 then
+	 if not (Int.equal ar1 (List.length cl1)) then
 	   Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in
        let _ =
-	 if ar2 <> List.length cl2 then
+	 if not (Int.equal ar2 (List.length cl2)) then
 	   Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in
        Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2)  id
      ]
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index e1de8be82..2cc203ed5 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -272,7 +272,7 @@ let make_discr_match_el  =
 let make_discr_match_brl i =
   List.map_i
     (fun j (_,idl,patl,_) ->
-       if j=i
+       if Int.equal j i
        then (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_True_ref))
        else (Loc.ghost,idl,patl, mkGRef (Lazy.force coq_False_ref))
     )
@@ -309,7 +309,7 @@ let build_constructors_of_type ind' argl =
 		    construct
 		in
 		let argl =
-		  if argl = []
+		  if List.is_empty argl
 		  then
  		    Array.to_list
 		      (Array.init (cst_narg - npar) (fun _ -> mkGHole ())
@@ -350,7 +350,7 @@ let add_pat_variables pat typ env : Environ.env =
 	    with Not_found -> assert false
 	  in
 	  let constructors = Inductiveops.get_constructors env indf in
-	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> cs.Inductiveops.cs_cstr = c) (Array.to_list constructors) in
+	  let constructor : Inductiveops.constructor_summary = List.find (fun cs -> eq_constructor c cs.Inductiveops.cs_cstr) (Array.to_list constructors) in
 	  let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
 	  List.fold_left2 add_pat_variables env patl (List.rev cs_args_types)
   in
@@ -397,7 +397,7 @@ let rec pattern_to_term_and_type env typ  = function
 	with Not_found -> assert false
       in
       let constructors = Inductiveops.get_constructors env indf in
-      let constructor  = List.find (fun cs -> cs.Inductiveops.cs_cstr = constr) (Array.to_list constructors) in
+      let constructor  = List.find (fun cs -> eq_constructor cs.Inductiveops.cs_cstr constr) (Array.to_list constructors) in
       let cs_args_types :types list = List.map (fun (_,_,t) -> t) constructor.Inductiveops.cs_args in
       let _,cstl = Inductiveops.dest_ind_family indf in
       let csta = Array.of_list cstl in
@@ -620,7 +620,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 			       Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	in
 	let case_pats = build_constructors_of_type ind [] in
-	assert (Array.length case_pats = 2);
+	assert (Int.equal (Array.length case_pats) 2);
 	let brl =
 	  List.map_i
 	    (fun i x -> (Loc.ghost,[],[case_pats.(i)],x))
@@ -652,7 +652,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 				 Printer.pr_glob_constr rt ++ str ". try again with a cast")
 	  in
 	  let case_pats = build_constructors_of_type ind nal_as_glob_constr in
-	  assert (Array.length case_pats = 1);
+	  assert (Int.equal (Array.length case_pats) 1);
 	  let br =
 	    (Loc.ghost,[],[case_pats.(0)],e)
 	  in
@@ -836,14 +836,14 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 
 let is_res id =
   try
-    String.sub (Id.to_string id) 0 4 = "_res"
+    String.equal (String.sub (Id.to_string id) 0 4) "_res"
   with Invalid_argument _ -> false
 
 
 
 let same_raw_term rt1 rt2 = 
   match rt1,rt2 with 
-    | GRef(_,r1), GRef (_,r2) -> r1=r2
+    | GRef(_,r1), GRef (_,r2) -> Globnames.eq_gr r1 r2
     | GHole _, GHole _ -> true
     | _ -> false
 let decompose_raw_eq lhs rhs = 
@@ -857,7 +857,7 @@ let decompose_raw_eq lhs rhs =
     observe (str "lrhs := " ++ int (List.length lrhs));
     let sllhs = List.length llhs in 
     let slrhs = List.length lrhs in 
-    if same_raw_term lhd rhd && sllhs = slrhs 
+    if same_raw_term lhd rhd && Int.equal sllhs slrhs 
     then
       (* let _ = assert false in  *)
       List.fold_right2 decompose_raw_eq	llhs lrhs acc
@@ -907,7 +907,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			assert false
 		end
 	    | GApp(loc1,GRef(loc2,eq_as_ref),[ty;GVar(loc3,id);rt])
-		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
+		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
 		  ->
 		begin
 		  try
@@ -1024,7 +1024,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     else new_b, Id.Set.add id id_to_exclude
 		  *)
 	    | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2])
-		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
+		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
 		  ->
 	      begin
 		try 
@@ -1116,7 +1116,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLetTuple(_,nal,(na,rto),t,b) ->
-	assert (rto=None);
+	assert (Option.is_empty rto);
 	begin
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let new_t,id_to_exclude' =
@@ -1207,7 +1207,7 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool)
 	   if Array.for_all
 	     (fun l ->
 		let (n',nt',is_defined') = List.nth l i in
-		n = n' && Notation_ops.eq_glob_constr nt nt' && is_defined = is_defined')
+		Name.equal n n' && Notation_ops.eq_glob_constr nt nt' && (is_defined : bool) == is_defined')
 	     rels_params
 	   then
 	     l := param::!l
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 6b4fbeef4..a16b5f0fe 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -279,7 +279,7 @@ let rec alpha_rt excluded rt =
     | GLambda(loc,Name id,k,t,b) ->
 	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
-	  if new_id = id
+	  if Id.equal new_id id
 	  then t,b
 	  else
 	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
@@ -293,7 +293,7 @@ let rec alpha_rt excluded rt =
 	let new_id = Namegen.next_ident_away id excluded in
 	let new_excluded = new_id::excluded in
 	let t,b =
-	  if new_id = id
+	  if Id.equal new_id id
 	  then t,b
 	  else
 	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
@@ -305,7 +305,7 @@ let rec alpha_rt excluded rt =
     | GLetIn(loc,Name id,t,b) ->
 	let new_id = Namegen.next_ident_away id excluded in
 	let t,b =
-	  if new_id = id
+	  if Id.equal new_id id
 	  then t,b
 	  else
 	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
@@ -325,7 +325,7 @@ let rec alpha_rt excluded rt =
 		 | Anonymous -> (na::nal,excluded,mapping)
 		 | Name id ->
 		     let new_id = Namegen.next_ident_away id excluded in
-		     if new_id = id
+		     if Id.equal new_id id
 		     then
 		       na::nal,id::excluded,mapping
 		     else
@@ -391,7 +391,7 @@ let is_free_in id =
     | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) ->
 	let check_in_b =
 	  match n with
-	    | Name id' -> Id.compare id' id <> 0
+	    | Name id' -> not (Id.equal id' id)
 	    | _ -> true
 	in
 	is_free_in t || (check_in_b && is_free_in b)
@@ -400,7 +400,7 @@ let is_free_in id =
 	  List.exists is_free_in_br brl
     | GLetTuple(_,nal,_,b,t) ->
 	let check_in_nal =
-	  not (List.exists (function Name id' -> id'= id | _ -> false) nal)
+	  not (List.exists (function Name id' -> Id.equal id' id | _ -> false) nal)
 	in
 	is_free_in t  || (check_in_nal && is_free_in b)
 
@@ -481,7 +481,7 @@ let replace_var_by_term x_id term =
 		 replace_var_by_pattern b
 		)
       | GLetTuple(_,nal,_,_,_)
-	  when List.exists (function Name id -> id = x_id | _ -> false) nal  ->
+	  when List.exists (function Name id -> Id.equal id x_id | _ -> false) nal  ->
 	  rt
       | GLetTuple(loc,nal,(na,rto),def,b) ->
 	  GLetTuple(loc,
@@ -527,7 +527,7 @@ let rec are_unifiable_aux  = function
       match eq with
 	 | PatVar _,_ | _,PatVar _ -> are_unifiable_aux eqs
 	 | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) ->
-	     if constructor2 <> constructor1
+	     if not (eq_constructor constructor2 constructor1)
 	     then raise NotUnifiable
 	     else
 	       let eqs' =
@@ -549,7 +549,7 @@ let rec eq_cases_pattern_aux  = function
       match eq with
 	 | PatVar _,PatVar _ -> eq_cases_pattern_aux eqs
 	 | PatCstr(_,constructor1,cpl1,_),PatCstr(_,constructor2,cpl2,_) ->
-	     if constructor2 <> constructor1
+	     if not (eq_constructor constructor2 constructor1)
 	     then raise NotUnifiable
 	     else
 	       let eqs' =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 993f3d5fb..e042240e2 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -376,7 +376,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
     in
     match wf_arg with
       | None ->
-	if List.length names = 1 then 1
+	if Int.equal (List.length names) 1 then 1
 	else error "Recursive argument must be specified"
       | Some wf_arg ->
 	  List.index (Name wf_arg) names
@@ -437,7 +437,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 		(function
 		   | Constrexpr.LocalRawAssum(l,k,t) ->
 		       List.exists
-			 (function (_,Name id) -> id =  wf_args | _ -> false)
+			 (function (_,Name id) -> Id.equal id wf_args | _ -> false)
 			 l
 		   | _ -> false
 		)
@@ -519,9 +519,9 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	      let nassoc = make_assoc assoc old_nal' nal in
 	      let assum = LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
 	      rebuild_bl ((assum :: aux), nassoc) bl' 
-		(if new_nal' = [] && rest = []
-		 then  typ' 
-		 else if new_nal' = [] 
+		(if List.is_empty new_nal' && List.is_empty rest
+		 then typ'
+		 else if List.is_empty new_nal'
 		 then CProdN(Loc.ghost,rest,typ')
 		 else CProdN(Loc.ghost,((new_nal',bk',nal't)::rest),typ'))
 	    else 
@@ -552,7 +552,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
 
 let do_generate_principle on_error register_built interactive_proof
     (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) :unit =
-  List.iter (fun (_,l) -> if l <> [] then error "Function does not support notations for now") fixpoint_exprl;
+  List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
   let _is_struct =
     match fixpoint_exprl with
       | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] ->
@@ -633,7 +633,7 @@ let rec add_args id new_args b =
   match b with
   | CRef r ->
       begin      match r with
-	| Libnames.Ident(loc,fname) when fname = id ->
+	| Libnames.Ident(loc,fname) when Id.equal fname id ->
 	    CAppExpl(Loc.ghost,(None,r),new_args)
 	| _ -> b
       end
@@ -651,7 +651,7 @@ let rec add_args id new_args b =
   | CAppExpl(loc,(pf,r),exprl) ->
       begin
 	match r with
-	| Libnames.Ident(loc,fname) when fname = id ->
+	| Libnames.Ident(loc,fname) when Id.equal fname id ->
 	    CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl))
 	| _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl)
       end
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 00a44888f..bba8564fa 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -714,7 +714,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 let generalize_dependent_of x hyp g =
   tclMAP
     (function
-       | (id,None,t) when not (id = hyp) &&
+       | (id,None,t) when not (Id.equal id hyp) &&
 	   (Termops.occur_var (pf_env g) x t) -> tclTHEN (h_generalize [mkVar id]) (thin [id])
        | _ -> tclIDTAC
     )
@@ -1037,7 +1037,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	 if the block contains only one function we can safely reuse [f_rect]
       *)
       try
-	if Array.length funs_constr <> 1 then raise Not_found;
+	if not (Int.equal (Array.length funs_constr) 1) then raise Not_found;
 	[| find_induction_principle funs_constr.(0) |]
       with Not_found ->
 	  Array.of_list
@@ -1137,7 +1137,7 @@ let revert_graph kn post_tac hid g =
     match kind_of_term typ with
       | App(i,args) when isInd i ->
 	  let ((kn',num) as ind') = destInd i in
-	  if kn = kn'
+	  if MutInd.equal kn kn'
 	  then (* We have generated a graph hypothesis so that we must change it if we can *)
 	    let info =
 	      try find_Function_of_graph ind'
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 65b4101a0..b7c471f4a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -63,7 +63,7 @@ let string_of_name nme = Id.to_string (id_of_name nme)
 (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
 let isVarf f x =
     match x with
-      | GVar (_,x) -> Pervasives.compare x f = 0
+      | GVar (_,x) -> Id.equal x f
       | _ -> false
 
 (** [ident_global_exist id] returns true if identifier [id] is linked
@@ -361,8 +361,8 @@ let ind2name = Id.of_string "__ind2"
 let verify_inds mib1 mib2 =
   if not mib1.mind_finite then error "First argument is coinductive";
   if not mib2.mind_finite then error "Second argument is coinductive";
-  if mib1.mind_ntypes <> 1 then error "First argument is mutual";
-  if mib2.mind_ntypes <> 1 then error "Second argument is mutual";
+  if not (Int.equal mib1.mind_ntypes 1) then error "First argument is mutual";
+  if not (Int.equal mib2.mind_ntypes 1) then error "Second argument is mutual";
   ()
 
 (*
@@ -598,7 +598,7 @@ let rec merge_types shift accrec1
   let res =
     match ltyp1 with
       | [] ->
-          let isrec1 = (accrec1<>[]) in
+          let isrec1 = not (List.is_empty accrec1) in
           let isrec2 = find_app ind2name ltyp2 in
           let rechyps =
             if isrec1 && isrec2
@@ -656,7 +656,7 @@ let build_link_map_aux (allargs1:Id.t array) (allargs2:Id.t array)
     (lnk:int merged_arg array) =
   Array.fold_left_i
     (fun i acc e ->
-      if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *)
+      if Int.equal i (Array.length lnk - 1) then acc (* functional arg, not in allargs *)
       else
         match e with
           | Prm_linked j | Arg_linked j -> Id.Map.add allargs2.(i) allargs1.(j) acc
@@ -922,7 +922,7 @@ let merge (id1:Id.t) (id2:Id.t) (args1:Id.t array)
                  as above: vars may be linked inside args2?? *)
     Array.mapi
       (fun i c ->
-        match Array.findi (fun i x -> x=c) args1 with
+        match Array.findi (fun i x -> Id.equal x c) args1 with
           | Some j -> Linked j
           | None -> Unlinked)
       args2 in
@@ -939,7 +939,7 @@ let remove_last_arg c =
   let xnolast = List.rev (List.tl (List.rev x)) in
   compose_prod xnolast y
 
-let rec remove_n_fst_list n l = if n=0 then l else remove_n_fst_list (n-1) (List.tl l)
+let rec remove_n_fst_list n l = if Int.equal n 0 then l else remove_n_fst_list (n-1) (List.tl l)
 let remove_n_last_list n l = List.rev (remove_n_fst_list n (List.rev l))
 
 let remove_last_n_arg n c =
@@ -961,7 +961,7 @@ let funify_branches relinfo nfuns branch =
       | _ -> assert false in
   let is_dom c =
     match kind_of_term c with
-      | Ind((u,_)) | Construct((u,_),_) -> u = mut_induct
+      | Ind((u,_)) | Construct((u,_),_) -> MutInd.equal u mut_induct
       | _ -> false in
   let _dom_i c =
     assert (is_dom c);
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 831fab633..49a90e432 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -155,7 +155,7 @@ let coq_conj = function () -> find_reference Coqlib.logic_module_name "conj"
 let f_S t = mkApp(delayed_force coq_S, [|t|]);;
 
 let rec n_x_id ids n =
-  if n = 0 then []
+  if Int.equal n 0 then []
   else let x = next_ident_away_in_goal x_id ids in
           x::n_x_id (x::ids) (n-1);;
 
@@ -1204,7 +1204,7 @@ let is_rec_res id =
   let rec_res_name = Id.to_string rec_res_id   in
   let id_name = Id.to_string id in
   try
-    String.sub id_name 0 (String.length rec_res_name) = rec_res_name
+    String.equal (String.sub id_name 0 (String.length rec_res_name)) rec_res_name
   with Invalid_argument _ -> false
  
 let clear_goals =
@@ -1277,7 +1277,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 		    (fun g ->
 		       let ids' = pf_ids_of_hyps g in
 		       lid := List.rev (List.subtract ids' ids);
-		       if !lid = [] then lid := [hid];
+		       if List.is_empty !lid then lid := [hid];
 		       tclIDTAC g
 		    )
 		    g
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index e31eba4e0..286fa6335 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -136,7 +136,7 @@ type term =
 
 let const n =
   if eq_num n num_0 then Zero else Const n
-let pow(p,i) = if i=1 then p else Pow(p,i)
+let pow(p,i) = if Int.equal i 1 then p else Pow(p,i)
 let add = function
     (Zero,q) -> q
   | (p,Zero) -> p
@@ -192,7 +192,7 @@ let rec mkt_pos n =
     mkt_app pxI [mkt_pos (quo_num n num_2)]
 
 let mkt_n n =
-  if n=num_0
+  if Num.eq_num n num_0
   then Lazy.force nN0
   else mkt_app nNpos [mkt_pos n]
 
@@ -212,7 +212,7 @@ let rec mkt_term t  =  match t with
 | Add (t1,t2) -> mkt_app  ttadd [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Sub (t1,t2) -> mkt_app  ttsub [Lazy.force tz; mkt_term t1; mkt_term t2]
 | Mul (t1,t2) -> mkt_app  ttmul [Lazy.force tz; mkt_term t1; mkt_term t2]
-| Pow (t1,n) ->  if (n = 0) then
+| Pow (t1,n) ->  if Int.equal n 0 then
     mkt_app ttconst [Lazy.force tz; mkt_z num_1]
 else
     mkt_app ttpow [Lazy.force tz; mkt_term t1; mkt_n (num_of_int n)]
@@ -311,7 +311,7 @@ let term_pol_sparse np t=
     match t with
     | Zero -> zeroP
     | Const r ->
-	if r = num_0
+	if Num.eq_num r num_0
 	then zeroP
 	else polconst d (Poly.Pint (Coef.of_num r))
     | Var v ->
@@ -365,19 +365,19 @@ let pol_sparse_to_term n2 p =
 		if m.(k)>0
 		then i0:=k
 	      done;
-	      if !i0 = 0
+	      if Int.equal !i0 0
 	      then (r,d)
 	      else if !i0 > r
 	      then (!i0, m.(!i0))
-	      else if !i0 = r && m.(!i0)<d
+	      else if Int.equal !i0 r && m.(!i0)<d
 	      then (!i0, m.(!i0))
 	      else (r,d))
 	  (0,0)
 	  p in
-      if i0=0
+      if Int.equal i0 0
       then
 	let mp = ref (polrec_to_term a) in
-        if p1=[]
+        if List.is_empty p1
 	then !mp
 	else add(!mp,aux p1)
       else (
@@ -391,7 +391,7 @@ let pol_sparse_to_term n2 p =
 	     else p2:=(a,m)::(!p2))
 	  p;
 	let vm =
-	  if e0=1
+	  if Int.equal e0 1
 	  then Var (string_of_int (i0))
 	  else pow (Var (string_of_int (i0)),e0) in
 	add(mul(vm, aux (List.rev (!p1))), aux (List.rev (!p2))))
@@ -401,11 +401,11 @@ let pol_sparse_to_term n2 p =
 
 let remove_list_tail l i =
   let rec aux l i =
-    if l=[]
+    if List.is_empty l
     then []
     else if i<0
     then l
-    else if i=0
+    else if Int.equal i 0
     then List.tl l
     else
       match l with
@@ -523,7 +523,7 @@ let theoremedeszeros_termes lp =
 	  let (cert,lp0,p,_lct) = theoremedeszeros lpol p in
           info "cert ok\n";
 	  let lc = cert.last_comb::List.rev cert.gb_comb in
-	  match remove_zeros (fun x -> x=zeroP) lc with
+	  match remove_zeros (fun x -> equal x zeroP) lc with
 	  | [] -> assert false
 	  | (lq::lci) ->
 	      (* lci commence par les nouveaux polynomes *)
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index ca6d305e8..78883a660 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -168,7 +168,7 @@ exception Failed
 let rec equal p q =
   match (p,q) with
       (Pint a,Pint b) -> C.equal a b
-    |(Prec(x,p1),Prec(y,q1)) -> (x=y) && Array.for_all2 equal p1 q1
+    |(Prec(x,p1),Prec(y,q1)) -> (Int.equal x y) && Array.for_all2 equal p1 q1
     | (_,_) -> false
 
 (* normalize polynomial: remove head zeros, coefficients are normalized
@@ -184,8 +184,8 @@ let norm p = match p with
 	 n:=!n-1;
        done;
        if !n<0 then Pint coef0
-       else if !n=0 then a.(0)
-       else if !n=d then p
+       else if Int.equal !n 0 then a.(0)
+       else if Int.equal !n d then p
        else (let b=Array.make (!n+1) (Pint coef0) in
                for i=0 to !n do b.(i)<-a.(i);done;
                Prec(x,b))
@@ -194,7 +194,7 @@ let norm p = match p with
 (* degree in v, v >= max var of p *)
 let deg v p =
   match p with
-      Prec(x,p1) when x=v -> Array.length p1 -1
+      Prec(x,p1) when Int.equal x v -> Array.length p1 -1
     |_ -> 0
 
 
@@ -214,8 +214,8 @@ let rec copyP p =
 (* coefficient of degree i in v, v >= max var of p *)
 let coef v i p =
   match p with
-      Prec (x,p1) when x=v  -> if i<(Array.length p1) then p1.(i) else Pint coef0
-    |_ -> if i=0 then p else Pint coef0
+      Prec (x,p1) when Int.equal x v  -> if i<(Array.length p1) then p1.(i) else Pint coef0
+    |_ -> if Int.equal i 0 then p else Pint coef0
 
 (* addition *)
 
@@ -272,7 +272,7 @@ let rec vars=function
 (* multiply p by v^n, v >= max_var p *)
 let multx n v p =
   match p with
-      Prec (x,p1) when x=v -> let p2= Array.make ((Array.length p1)+n) (Pint coef0) in
+      Prec (x,p1) when Int.equal x v -> let p2= Array.make ((Array.length p1)+n) (Pint coef0) in
         for i=0 to (Array.length p1)-1 do
           p2.(i+n)<-p1.(i);
         done;
@@ -311,9 +311,9 @@ let rec multP p q =
 let deriv v p =
   match p with
       Pint a -> Pint coef0
-    | Prec(x,p1) when x=v ->
+    | Prec(x,p1) when Int.equal x v ->
        let d = Array.length p1 -1 in
-         if d=1 then p1.(1)
+         if Int.equal d 1 then p1.(1)
          else
            (let p2 = Array.make d (Pint coef0) in
               for i=0 to d-1 do
@@ -410,7 +410,7 @@ let rec string_of_Pcut p =
       and s=ref ""
       and sp=ref "" in
     let st0 = string_of_Pcut t.(0) in
-      if st0<>"0"
+      if not (String.equal st0 "0")
       then s:=st0;
     let fin = ref false in
     for i=(Array.length t)-1 downto 1 do
@@ -421,31 +421,31 @@ let rec string_of_Pcut p =
       else (
 	let si=string_of_Pcut  t.(i) in
 	sp:="";
-	if i=1
+	if Int.equal i 1
 	then (
-	  if si<>"0"
+	  if not (String.equal si "0")
 	  then (nsP:=(!nsP)-1;
-		if si="1"
+		if String.equal si "1"
 		then sp:=v
 		else
 		  (if (String.contains si '+')
 		  then sp:="("^si^")*"^v
 		  else sp:=si^"*"^v)))
 	else (
-	  if si<>"0"
+	  if not (String.equal si "0")
 	  then (nsP:=(!nsP)-1;
-		if si="1"
+		if String.equal si "1"
 		then sp:=v^"^"^(string_of_int i)
 		else (if (String.contains si '+')
 		then sp:="("^si^")*"^v^"^"^(string_of_int i)
 		else  sp:=si^"*"^v^"^"^(string_of_int i))));
-	if !sp<>"" && not (!fin)
+	if not (String.is_empty !sp) && not (!fin)
 	then (nsP:=(!nsP)-1;
-	      if !s=""
+	      if String.is_empty !s
 	      then s:=!sp
 	      else s:=(!s)^"+"^(!sp)));
     done;
-    if !s="" then (nsP:=(!nsP)-1;
+    if String.is_empty !s then (nsP:=(!nsP)-1;
 		   (s:="0"));
     !s
 
@@ -468,7 +468,7 @@ let print_lpoly lp = print_tpoly (Array.of_list lp)
 
 (* return (s,r) s.t. p = s*q+r *)
 let rec quo_rem_pol p q x =
-  if x=0
+  if Int.equal x 0
   then (match (p,q) with
           |(Pint a, Pint b) ->
 	     if C.equal (C.modulo a b) coef0
@@ -532,7 +532,7 @@ let div_pol_rat p q=
 let pseudo_div p q x =
   match q with
       Pint _ -> (cf0, q,1, p)
-    | Prec (v,q1) when x<>v -> (cf0, q,1, p)
+    | Prec (v,q1) when not (Int.equal x v) -> (cf0, q,1, p)
     | Prec (v,q1) ->
 	(
 	  (*  pr "pseudo_division: c^d*p = s*q + r";*)
@@ -569,13 +569,13 @@ and pgcd_pol p q x =
 
 and content_pol p x =
   match p with
-      Prec(v,p1) when v=x ->
+      Prec(v,p1) when Int.equal v x ->
         Array.fold_left (fun a b -> pgcd_pol_rec a b (x-1)) cf0 p1
     | _ -> p
 
 and pgcd_coef_pol c p x =
   match p with
-      Prec(v,p1) when x=v ->
+      Prec(v,p1) when Int.equal x v ->
         Array.fold_left (fun a b -> pgcd_pol_rec a b (x-1)) c  p1
     |_ -> pgcd_pol_rec c p (x-1)
 
@@ -587,9 +587,9 @@ and pgcd_pol_rec p q x =
 	  then q
 	  else if equal q cf0
 	  then p
-	  else if (deg x q) = 0
+	  else if Int.equal (deg x q) 0
 	  then pgcd_coef_pol q p x
-	  else if (deg x p) = 0
+	  else if Int.equal (deg x p) 0
 	  then pgcd_coef_pol p q x
 	  else (
 	    let a = content_pol p x in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 0dd137b6f..c39b2ff0a 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -131,7 +131,7 @@ let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
 
 let rev_assoc k =
   let rec loop = function
-    | [] -> raise Not_found | (v,k')::_ when k = k' -> v | _ :: l -> loop l
+    | [] -> raise Not_found | (v,k')::_ when Int.equal k k' -> v | _ :: l -> loop l
   in
   loop
 
@@ -676,7 +676,7 @@ let rec shuffle p (t1,t2) =
 let shuffle_mult p_init k1 e1 k2 e2 =
   let rec loop p = function
     | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
-	if v1 = v2 then
+	if Int.equal v1 v2 then
           let tac =
             clever_rewrite p [[P_APP 1; P_APP 1; P_APP 1; P_APP 1];
                               [P_APP 1; P_APP 1; P_APP 1; P_APP 2];
@@ -733,7 +733,7 @@ let shuffle_mult p_init k1 e1 k2 e2 =
 let shuffle_mult_right p_init e1 k2 e2 =
   let rec loop p = function
     | (({c=c1;v=v1}::l1) as l1'),(({c=c2;v=v2}::l2) as l2') ->
-	if v1 = v2 then
+	if Int.equal v1 v2 then
           let tac =
             clever_rewrite p
               [[P_APP 1; P_APP 1; P_APP 1];
@@ -964,7 +964,7 @@ let reduce_factor p = function
 
 let rec condense p = function
   | Oplus(f1,(Oplus(f2,r) as t)) ->
-      if weight f1 = weight f2 then begin
+      if Int.equal (weight f1) (weight f2) then begin
 	let shrink_tac,t = shrink_pair (P_APP 1 :: p) f1 f2 in
 	let assoc_tac =
           clever_rewrite p
@@ -980,7 +980,7 @@ let rec condense p = function
   | Oplus(f1,Oz n) ->
       let tac,f1' = reduce_factor (P_APP 1 :: p) f1 in tac,Oplus(f1',Oz n)
   | Oplus(f1,f2) ->
-      if weight f1 = weight f2 then begin
+      if Int.equal (weight f1) (weight f2) then begin
 	let tac_shrink,t = shrink_pair p f1 f2 in
 	let tac,t' = condense p t in
 	tac_shrink :: tac,t'
@@ -1143,7 +1143,7 @@ let replay_history tactic_normalisation =
 	  and eq2 = val_of(decompile e2) in
 	  let kk = mk_integer k in
 	  let state_eq = mk_eq eq1 (mk_times eq2 kk) in
-	  if e1.kind = DISE then
+	  if e1.kind == DISE then
             let tac = scalar_norm [P_APP 3] e2.body in
             tclTHENS
 	      (cut state_eq)
@@ -1254,7 +1254,7 @@ let replay_history tactic_normalisation =
 	  and id2 = hyp_of_tag e2.id in
 	  let eq1 = val_of(decompile e1)
 	  and eq2 = val_of(decompile e2) in
-	  if k1 =? one && e2.kind = EQUA then
+	  if k1 =? one && e2.kind == EQUA then
             let tac_thm =
               match e1.kind with
 		| EQUA -> Lazy.force coq_OMEGA5
@@ -1263,7 +1263,7 @@ let replay_history tactic_normalisation =
 	    in
             let kk = mk_integer k2 in
             let p_initial =
-              if e1.kind=DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
+              if e1.kind == DISE then [P_APP 1; P_TYPE] else [P_APP 2; P_TYPE] in
             let tac = shuffle_mult_right p_initial e1.body k2 e2.body in
             tclTHENLIST [
 	      (generalize_tac
@@ -1331,7 +1331,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
       (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
       (tclTRY (clear [id]))
   in
-  if tac <> [] then
+  if not (List.is_empty tac) then
     let id' = new_identifier () in
     ((id',(tclTHENLIST [ (shift_left); (mk_then tac); (intros_using [id']) ]))
           :: tactic,
@@ -1340,12 +1340,12 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
     (tactic,defs)
 
 let destructure_omega gl tac_def (id,c) =
-  if atompart_of_id id = "State" then
+  if String.equal (atompart_of_id id) "State" then
     tac_def
   else
     try match destructurate_prop c with
       | Kapp(Eq,[typ;t1;t2])
-	when destructurate_type (pf_nf gl typ) = Kapp(Z,[]) ->
+	when begin match destructurate_type (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end ->
 	  let t = mk_plus t1 (mk_inv t2) in
 	  normalize_equation
 	    id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index c09e2d743..92b27c3e8 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -207,7 +207,7 @@ let compute_lhs typ i nargsi =
 let compute_rhs bodyi index_of_f =
   let rec aux c =
     match kind_of_term c with
-      | App (j, args) when isRel j && destRel j = index_of_f (* recursive call *) ->
+      | App (j, args) when isRel j && Int.equal (destRel j) index_of_f (* recursive call *) ->
           let i = destRel (Array.last args) in
 	  PMeta (Some (coerce_meta_in i))
       | App (f,args) ->
@@ -239,7 +239,7 @@ let compute_ivs gl f cs =
            (* REL nargsi+1 to REL nargsi + nargs3 are arguments of f *)
            (* REL 1 to REL nargsi are argsi (reverse order) *)
            (* First we test if the RHS is the RHS for constants *)
-                   if isRel bodyi && destRel bodyi = 1 then
+                   if isRel bodyi && Int.equal (destRel bodyi) 1 then
                      c_lhs := Some (compute_lhs (snd (List.hd args3))
                                       i nargsi)
            (* Then we test if the RHS is the RHS for variables *)
@@ -260,7 +260,7 @@ let compute_ivs gl f cs =
                    end)
                 lci;
 
-              if !c_lhs = None && !v_lhs = None then i_can't_do_that ();
+              if Option.is_empty !c_lhs && Option.is_empty !v_lhs then i_can't_do_that ();
 
 	      (* The Cases predicate is a lambda; we assume no dependency *)
 	      let p = match kind_of_term p with
@@ -338,8 +338,8 @@ let path_of_int n =
   (* returns the list of digits of n in reverse order with
      initial 1 removed *)
   let rec digits_of_int n =
-    if n=1 then []
-    else (n mod 2 = 1)::(digits_of_int (n lsr 1))
+    if Int.equal n 1 then []
+    else (Int.equal (n mod 2) 1)::(digits_of_int (n lsr 1))
   in
   List.fold_right
     (fun b c -> mkApp ((if b then Lazy.force coq_Right_idx
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e8a72c055..635fc366f 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -38,6 +38,10 @@ type direction = Left of int | Right of int
 type occ_step = O_left | O_right | O_mono
 type occ_path = occ_step list
 
+let occ_step_eq s1 s2 = match s1, s2 with
+| O_left, O_left | O_right, O_right | O_mono, O_mono -> true
+| _ -> false
+
 (* chemin identifiant une proposition sous forme du nom de l'hypothèse et
    d'une liste de pas à partir de la racine de l'hypothèse *)
 type occurence = {o_hyp : Names.Id.t; o_path : occ_path}
@@ -209,7 +213,7 @@ let intern_omega_force env t v = env.om_vars <- (t,v) :: env.om_vars
 let unintern_omega env id =
   let rec loop = function
 	[] -> failwith "unintern"
-      | ((t,j)::l) -> if id = j then t else loop l in
+      | ((t,j)::l) -> if Int.equal id j then t else loop l in
   loop env.om_vars
 
 (* \subsection{Gestion des environnements de variable pour la réflexion}
@@ -484,8 +488,8 @@ let shuffle_path k1 e1 k2 e2 =
   let rec loop = function
       (({c=c1;v=v1}::l1) as l1'),
       (({c=c2;v=v2}::l2) as l2') ->
-	if v1 = v2 then
-          if k1*c1 + k2 * c2 = zero then (
+	if Int.equal v1 v2 then
+          if Bigint.equal (k1 * c1 + k2 * c2) zero then (
             Lazy.force coq_f_cancel :: loop (l1,l2))
           else (
             Lazy.force coq_f_equal :: loop (l1,l2) )
@@ -563,7 +567,7 @@ let reduce_factor = function
 
 let rec condense env = function
     Oplus(f1,(Oplus(f2,r) as t)) ->
-      if weight env f1 = weight env f2 then begin
+      if Int.equal (weight env f1) (weight env f2) then begin
 	let shrink_tac,t = shrink_pair f1 f2 in
 	let assoc_tac = Lazy.force coq_c_plus_assoc_l in
 	let tac_list,t' = condense env (Oplus(t,r)) in
@@ -577,7 +581,7 @@ let rec condense env = function
       let tac,f1' = reduce_factor f1 in
       [do_left (do_list tac)],Oplus(f1',Oint n)
   | Oplus(f1,f2) ->
-      if weight env f1 = weight env f2 then begin
+      if Int.equal (weight env f1) (weight env f2) then begin
 	let tac_shrink,t = shrink_pair f1 f2 in
 	let tac,t' = condense env t in
 	tac_shrink :: tac,t'
@@ -595,12 +599,12 @@ let rec condense env = function
 (* \subsection{Elimination des zéros} *)
 
 let rec clear_zero = function
-   Oplus(Omult(Oatom v,Oint n),r) when n=zero ->
+   Oplus(Omult(Oatom v,Oint n),r) when Bigint.equal n zero ->
      let tac',t = clear_zero r in
      Lazy.force coq_c_red5 :: tac',t
   | Oplus(f,r) ->
       let tac,t = clear_zero r in
-      (if tac = [] then [] else [do_right (do_list tac)]),Oplus(f,t)
+      (if List.is_empty tac then [] else [do_right (do_list tac)]),Oplus(f,t)
   | t -> [],t;;
 
 (* \subsection{Transformation des hypothèses} *)
@@ -1014,10 +1018,10 @@ let rec solve_with_constraints all_solutions path =
 let find_path {o_hyp=id;o_path=p} env =
   let rec loop_path = function
       ([],l) -> Some l
-    | (x1::l1,x2::l2) when x1 = x2 -> loop_path (l1,l2)
+    | (x1::l1,x2::l2) when occ_step_eq x1 x2 -> loop_path (l1,l2)
     | _ -> None in
   let rec loop_id i = function
-      CCHyp{o_hyp=id';o_path=p'} :: l when id = id' ->
+      CCHyp{o_hyp=id';o_path=p'} :: l when Names.Id.equal id id' ->
 	begin match loop_path (p',p) with
 	  Some r -> i,r
 	| None -> loop_id (succ i) l
@@ -1260,7 +1264,7 @@ let resolution env full_reified_goal systems_list =
       let i = List.index0 e.e_origin.o_hyp l_hyps in
       (* PL: it seems that additionnally introduced hyps are in the way during
              normalization, hence this index shifting... *)
-      if i=0 then 0 else Pervasives.(+) i (List.length to_introduce)
+      if Int.equal i 0 then 0 else Pervasives.(+) i (List.length to_introduce)
     in
     app coq_pair_step [| mk_nat correct_index; loop e.e_origin.o_path |] in
   let normalization_trace =
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 75005f1c8..9aad65f29 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -160,7 +160,7 @@ let rec fill stack proof =
     | slice::super ->
 	if
 	  !pruning &&
-	  slice.proofs_done=[] &&
+	  List.is_empty slice.proofs_done &&
 	  not (slice.changes_goal && proof.dep_goal) &&
 	  not (Int.Set.exists
 		 (fun i -> Int.Set.mem i proof.dep_hyps)
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 5a77bf967..96758788a 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -95,7 +95,7 @@ let rec make_form atom_env gls term =
 	Prod(_,a,b) ->
 	  if not (Termops.dependent (mkRel 1) b) &&
 	    Retyping.get_sort_family_of
-	    (pf_env gls) (Tacmach.project gls) a = InProp
+	    (pf_env gls) (Tacmach.project gls) a == InProp
 	  then
 	    let fa=make_form atom_env gls a in
 	    let fb=make_form atom_env gls b in
@@ -105,19 +105,19 @@ let rec make_form atom_env gls term =
       | Cast(a,_,_) ->
 	  make_form atom_env gls a
       | Ind ind ->
-	  if ind = Lazy.force li_False then
+	  if Names.eq_ind ind (Lazy.force li_False) then
 	    Bot
 	  else
 	    make_atom atom_env (normalize term)
-      | App(hd,argv) when Array.length argv = 2 ->
+      | App(hd,argv) when Int.equal (Array.length argv) 2 ->
 	  begin
 	    try
 	      let ind = destInd hd in
-		if ind = Lazy.force li_and then
+		if Names.eq_ind ind (Lazy.force li_and) then
 		  let fa=make_form atom_env gls argv.(0) in
 		  let fb=make_form atom_env gls argv.(1) in
 		    Conjunct (fa,fb)
-		else if ind = Lazy.force li_or then
+		else if Names.eq_ind ind (Lazy.force li_or) then
 		  let fa=make_form atom_env gls argv.(0) in
 		  let fb=make_form atom_env gls argv.(1) in
 		    Disjunct (fa,fb)
@@ -135,7 +135,7 @@ let rec make_hyps atom_env gls lenv = function
 	make_hyps atom_env gls (typ::lenv) rest in
 	if List.exists (Termops.dependent (mkVar id)) lenv ||
 	  (Retyping.get_sort_family_of
-	     (pf_env gls) (Tacmach.project gls) typ <> InProp)
+	     (pf_env gls) (Tacmach.project gls) typ != InProp)
 	then
 	  hrec
 	else
@@ -143,7 +143,7 @@ let rec make_hyps atom_env gls lenv = function
 
 let rec build_pos n =
   if n<=1 then force node_count l_xH
-  else if n land 1 = 0 then
+  else if Int.equal (n land 1) 0 then
     mkApp (force node_count l_xO,[|build_pos (n asr 1)|])
   else
     mkApp (force node_count l_xI,[|build_pos (n asr 1)|])
@@ -261,17 +261,16 @@ let rtauto_tac gls=
   let gl=pf_concl gls in
   let _=
     if Retyping.get_sort_family_of
-      (pf_env gls) (Tacmach.project gls) gl <> InProp
+      (pf_env gls) (Tacmach.project gls) gl != InProp
     then errorlabstrm "rtauto" (Pp.str "goal should be in Prop") in
   let glf=make_form gamma gls gl in
   let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in
   let formula=
     List.fold_left (fun gl (_,f)-> Arrow (f,gl)) glf hyps in
-  let search_fun =
-    if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then
-      Search.debug_depth_first
-    else
-      Search.depth_first in
+  let search_fun = match Tacinterp.get_debug() with
+  | Tactic_debug.DebugOn 0 -> Search.debug_depth_first
+  | _ -> Search.depth_first
+  in
   let _ =
     begin
       reset_info ();
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index f16c298af..30ceb1018 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -50,7 +50,7 @@ let tag_arg tag_rec map subs i c =
   match map i with
       Eval -> mk_clos subs c
     | Prot -> mk_atom c
-    | Rec -> if i = -1 then mk_clos subs c else tag_rec c
+    | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c
 
 let rec mk_clos_but f_map subs t =
   match f_map t with
@@ -423,7 +423,7 @@ let theory_to_obj : ring_info -> obj =
   let cache_th (name,th) = add_entry name th in
   declare_object
     {(default_object "tactic-new-ring-theory") with
-      open_function = (fun i o -> if i=1 then cache_th o);
+      open_function = (fun i o -> if Int.equal i 1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
       classify_function = (fun x -> Substitute x)}
@@ -730,7 +730,7 @@ VERNAC ARGUMENT EXTEND ring_mod
 END
 
 let set_once s r v =
-  if !r = None then r := Some v else error (s^" cannot be set twice")
+  if Option.is_empty !r then r := Some v else error (s^" cannot be set twice")
 
 let process_ring_mods l =
   let kind = ref None in
@@ -982,7 +982,7 @@ let ftheory_to_obj : field_info -> obj =
   let cache_th (name,th) = add_field_entry name th in
   declare_object
     {(default_object "tactic-new-field-theory") with
-      open_function = (fun i o -> if i=1 then cache_th o);
+      open_function = (fun i o -> if Int.equal i 1 then cache_th o);
       cache_function = cache_th;
       subst_function = subst_th;
       classify_function = (fun x -> Substitute x) }
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 180d15009..790e1970b 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -35,17 +35,17 @@ open Lazy
 
 let interp_ascii dloc p =
   let rec aux n p =
-     if n = 0 then [] else
+     if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     GRef (dloc,if mp = 0 then glob_false else glob_true)
+     GRef (dloc,if Int.equal mp 0 then glob_false else glob_true)
      :: (aux (n-1) (p/2)) in
   GApp (dloc,GRef(dloc,force glob_Ascii), aux 8 p)
 
 let interp_ascii_string dloc s =
   let p =
-    if String.length s = 1 then int_of_char s.[0]
+    if Int.equal (String.length s) 1 then int_of_char s.[0]
     else
-      if String.length s = 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
+      if Int.equal (String.length s) 3 && is_digit s.[0] && is_digit s.[1] && is_digit s.[2]
       then int_of_string s
       else
 	user_err_loc (dloc,"interp_ascii_string",
@@ -54,13 +54,13 @@ let interp_ascii_string dloc s =
 
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
-    | [] when n = 0 -> 0
-    | GRef (_,k)::l when k = glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | GRef (_,k)::l when k = glob_false -> 2*(uninterp_bool_list (n-1) l)
+    | [] when Int.equal n 0 -> 0
+    | GRef (_,k)::l when Globnames.eq_gr k glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | GRef (_,k)::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
   try
     let aux = function
-    | GApp (_,GRef (_,k),l) when k = force glob_Ascii -> uninterp_bool_list 8 l
+    | GApp (_,GRef (_,k),l) when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
   with
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index efbd140ee..545f205db 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -55,7 +55,7 @@ let r_of_posint dloc n =
       let (q,r) = div2_with_rest n in
       let b = GApp(dloc,GRef(dloc,glob_Rmult),[r2;r_of_pos q]) in
       if r then GApp(dloc,GRef(dloc,glob_Rplus),[r1;b]) else b in
-  if n <> zero then r_of_pos n else GRef(dloc,glob_R0)
+  if not (Bigint.equal n zero) then r_of_pos n else GRef(dloc,glob_R0)
 
 let r_of_int dloc z =
   if is_strictly_neg z then
@@ -72,34 +72,34 @@ let bignat_of_r =
 let rec bignat_of_pos = function
   (* 1+1 *)
   | GApp (_,GRef (_,p), [GRef (_,o1); GRef (_,o2)])
-      when p = glob_Rplus && o1 = glob_R1 && o2 = glob_R1 -> two
+      when Globnames.eq_gr p glob_Rplus && Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 -> two
   (* 1+(1+1) *)
   | GApp (_,GRef (_,p1), [GRef (_,o1);
       GApp(_,GRef (_,p2),[GRef(_,o2);GRef(_,o3)])])
-      when p1 = glob_Rplus && p2 = glob_Rplus &&
-           o1 = glob_R1 && o2 = glob_R1 && o3 = glob_R1 -> three
+      when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rplus &&
+           Globnames.eq_gr o1 glob_R1 && Globnames.eq_gr o2 glob_R1 && Globnames.eq_gr o3 glob_R1 -> three
   (* (1+1)*b *)
-  | GApp (_,GRef (_,p), [a; b]) when p = glob_Rmult ->
-      if bignat_of_pos a <> two then raise Non_closed_number;
+  | GApp (_,GRef (_,p), [a; b]) when Globnames.eq_gr p glob_Rmult ->
+      if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number;
       mult_2 (bignat_of_pos b)
   (* 1+(1+1)*b *)
   | GApp (_,GRef (_,p1), [GRef (_,o); GApp (_,GRef (_,p2),[a;b])])
-      when p1 = glob_Rplus && p2 = glob_Rmult && o = glob_R1  ->
-      if bignat_of_pos a <> two then raise Non_closed_number;
+      when Globnames.eq_gr p1 glob_Rplus && Globnames.eq_gr p2 glob_Rmult && Globnames.eq_gr o glob_R1  ->
+      if not (Bigint.equal (bignat_of_pos a) two) then raise Non_closed_number;
         add_1 (mult_2 (bignat_of_pos b))
   | _ -> raise Non_closed_number
 in
 let bignat_of_r = function
-  | GRef (_,a) when a = glob_R0 -> zero
-  | GRef (_,a) when a = glob_R1 -> one
+  | GRef (_,a) when Globnames.eq_gr a glob_R0 -> zero
+  | GRef (_,a) when Globnames.eq_gr a glob_R1 -> one
   | r -> bignat_of_pos r
 in
 bignat_of_r
 
 let bigint_of_r = function
-  | GApp (_,GRef (_,o), [a]) when o = glob_Ropp ->
+  | GApp (_,GRef (_,o), [a]) when Globnames.eq_gr o glob_Ropp ->
       let n = bignat_of_r a in
-      if n = zero then raise Non_closed_number;
+      if Bigint.equal n zero then raise Non_closed_number;
       neg n
   | a -> bignat_of_r a
 
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index e5e4e9331..67e54c017 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -47,7 +47,7 @@ let pos_of_bignat dloc x =
   let rec pos_of x =
     match div2_with_rest x with
       | (q,false) -> GApp (dloc, ref_xO,[pos_of q])
-      | (q,true) when q <> zero -> GApp (dloc,ref_xI,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> GApp (dloc,ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -65,9 +65,9 @@ let interp_positive dloc n =
 (**********************************************************************)
 
 let rec bignat_of_pos = function
-  | GApp (_, GRef (_,b),[a]) when b = glob_xO -> mult_2(bignat_of_pos a)
-  | GApp (_, GRef (_,b),[a]) when b = glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | GRef (_, a) when a = glob_xH -> Bigint.one
+  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
+  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | GRef (_, a) when Globnames.eq_gr a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
 
 let uninterp_positive p =
@@ -103,7 +103,7 @@ let glob_Npos = ConstructRef path_of_Npos
 let n_path = make_path binnums "N"
 
 let n_of_binnat dloc pos_or_neg n =
-  if n <> zero then
+  if not (Bigint.equal n zero) then
     GApp(dloc, GRef (dloc,glob_Npos), [pos_of_bignat dloc n])
   else
     GRef (dloc, glob_N0)
@@ -120,8 +120,8 @@ let n_of_int dloc n =
 (**********************************************************************)
 
 let bignat_of_n = function
-  | GApp (_, GRef (_,b),[a]) when b = glob_Npos -> bignat_of_pos a
-  | GRef (_, a) when a = glob_N0 -> Bigint.zero
+  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
+  | GRef (_, a) when Globnames.eq_gr a glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_n p =
@@ -154,7 +154,7 @@ let glob_POS = ConstructRef path_of_POS
 let glob_NEG = ConstructRef path_of_NEG
 
 let z_of_int dloc n =
-  if n <> zero then
+  if not (Bigint.equal n zero) then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
     GApp(dloc, GRef (dloc,sgn), [pos_of_bignat dloc n])
@@ -166,9 +166,9 @@ let z_of_int dloc n =
 (**********************************************************************)
 
 let bigint_of_z = function
-  | GApp (_, GRef (_,b),[a]) when b = glob_POS -> bignat_of_pos a
-  | GApp (_, GRef (_,b),[a]) when b = glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | GRef (_, a) when a = glob_ZERO -> Bigint.zero
+  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
+  | GApp (_, GRef (_,b),[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | GRef (_, a) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 let uninterp_z p =