Removing a bunch of generic equalities.

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

9 files changed, 62 insertions, 61 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3568535733..d249df5787 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 a01039eb0b..d11e810e13 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 7e229fbd2e..cb9d12c5e4 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 e1de8be82a..2cc203ed51 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 6b4fbeef46..a16b5f0fe5 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 993f3d5fb0..e042240e2d 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 00a44888fa..bba8564faa 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 65b4101a0f..b7c471f4ae 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 831fab633b..49a90e432a 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