More monomorphizations

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

16 files changed, 163 insertions, 117 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index deba56f73..1d2587efe 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -179,16 +179,17 @@ let push_local sz r =
 
 
 (*i Compilation of variables *)
-let find_at el l =
+let find_at f l =
   let rec aux n = function
     | [] -> raise Not_found
-    | hd :: tl -> if hd = el then n else aux (n+1) tl
+    | hd :: tl -> if f hd then n else aux (n + 1) tl
   in aux 1 l
 
 let pos_named id r =
   let env = !(r.in_env) in
   let cid = FVnamed id in
-  try Kenvacc(r.offset + env.size - (find_at cid env.fv_rev))
+  let f = function FVnamed id' -> id_eq id id' | _ -> false in
+  try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
   with Not_found ->
     let pos = env.size in
     r.in_env := { size = pos+1; fv_rev =  cid:: env.fv_rev};
@@ -206,7 +207,8 @@ let pos_rel i r sz =
       let i = i - r.nb_rec in
       let db = FVrel(i) in
       let env = !(r.in_env) in
-      try Kenvacc(r.offset + env.size - (find_at db env.fv_rev))
+      let f = function FVrel j -> Int.equal i j | _ -> false in
+      try Kenvacc(r.offset + env.size - (find_at f env.fv_rev))
       with Not_found ->
 	let pos = env.size in
 	r.in_env := { size = pos+1; fv_rev =  db:: env.fv_rev};
@@ -357,7 +359,7 @@ let rec str_const c =
 	    let oip = oib.mind_packets.(j) in
 	    let num,arity = oip.mind_reloc_tbl.(i-1) in
 	    let nparams = oib.mind_nparams in
-	    if nparams + arity = Array.length args then
+	    if Int.equal (nparams + arity) (Array.length args) then
               (* spiwack: *)
               (* 1/ tries to compile the constructor in an optimal way,
                     it is supposed to work only if the arguments are
@@ -609,7 +611,7 @@ let rec compile_constr reloc c sz cont =
       let lbl_sw = Label.create () in
       let sz_b,branch,is_tailcall =
 	match branch1 with
-	| Kreturn k -> assert (k = sz); sz, branch1, true
+	| Kreturn k -> assert (Int.equal k sz); sz, branch1, true
 	| _ -> sz+3, Kjump, false
       in
       let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
@@ -632,7 +634,7 @@ let rec compile_constr reloc c sz cont =
 	  let nargs = List.length args in
 	  let lbl_b,code_b =
 	    label_code(
-	    if nargs = arity then
+	    if Int.equal nargs arity then
 	      Kpushfields arity ::
 	      compile_constr (push_param arity sz_b reloc)
 		body (sz_b+arity) (add_pop arity (branch :: !c))
@@ -844,7 +846,7 @@ let op_compilation n op =
   fun kn fc reloc args sz cont ->
   if not fc then raise Not_found else
   let nargs = Array.length args in
-  if nargs=n then (*if it is a fully applied addition*)
+  if Int.equal nargs n then (*if it is a fully applied addition*)
     let (escape, labeled_cont) = make_branch cont in
     let else_lbl = Label.create () in
       comp_args compile_constr reloc args sz
@@ -854,7 +856,7 @@ let op_compilation n op =
            (* works as comp_app with nargs = n and non-tailcall cont*)
            Kgetglobal (get_allias !global_env kn)::
            Kapply n::labeled_cont)))
-  else if nargs=0 then
+  else if Int.equal nargs 0 then
     code_construct kn cont
   else
     comp_app (fun _ _ _ cont -> code_construct kn cont)
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 681fb8533..1c9b2145d 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -327,7 +327,7 @@ and fterm =
 
 let fterm_of v = v.term
 let set_norm v = v.norm <- Norm
-let is_val v = v.norm = Norm
+let is_val v = match v.norm with Norm -> true | _ -> false
 
 let mk_atom c = {norm=Norm;term=FAtom c}
 
@@ -426,9 +426,9 @@ let rec lft_fconstr n ft =
     | FLOCKED -> assert false
     | _ -> {norm=ft.norm; term=FLIFT(n,ft)}
 let lift_fconstr k f =
-  if k=0 then f else lft_fconstr k f
+  if Int.equal k 0 then f else lft_fconstr k f
 let lift_fconstr_vect k v =
-  if k=0 then v else Array.map (fun f -> lft_fconstr k f) v
+  if Int.equal k 0 then v else Array.map (fun f -> lft_fconstr k f) v
 
 let clos_rel e i =
   match expand_rel i e with
@@ -452,7 +452,7 @@ let compact_stack head stk =
 
 (* Put an update mark in the stack, only if needed *)
 let zupdate m s =
-  if !share & m.norm = Red
+  if !share && begin match m.norm with Red -> true | _ -> false end
   then
     let s' = compact_stack m s in
     let _ = m.term <- FLOCKED in
@@ -760,7 +760,7 @@ let rec reloc_rargs_rec depth stk =
   match stk with
       Zapp args :: s ->
         Zapp (lift_fconstr_vect depth args) :: reloc_rargs_rec depth s
-    | Zshift(k)::s -> if k=depth then s else reloc_rargs_rec (depth-k) s
+    | Zshift(k)::s -> if Int.equal k depth then s else reloc_rargs_rec (depth-k) s
     | _ -> stk
 
 let reloc_rargs depth stk =
@@ -771,13 +771,13 @@ let rec drop_parameters depth n argstk =
       Zapp args::s ->
         let q = Array.length args in
         if n > q then drop_parameters depth (n-q) s
-        else if n = q then reloc_rargs depth s
+        else if Int.equal n q then reloc_rargs depth s
         else
           let aft = Array.sub args n (q-n) in
           reloc_rargs depth (append_stack aft s)
     | Zshift(k)::s -> drop_parameters (depth-k) n s
     | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
-	if n=0 then []
+	if Int.equal n 0 then []
 	else anomaly
 	  "ill-typed term: found a match on a partially applied constructor"
     | _ -> assert false
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index b8edcae72..b995f2e4a 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -127,7 +127,7 @@ let subst_const_def sub = function
   | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
 
 let subst_const_body sub cb = {
-  const_hyps = (assert (cb.const_hyps=[]); []);
+  const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
   const_body = subst_const_def sub cb.const_body;
   const_type = subst_const_type sub cb.const_type;
   const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
@@ -341,7 +341,7 @@ let subst_mind sub mib =
   { mind_record = mib.mind_record ;
     mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
-    mind_hyps = (assert (mib.mind_hyps=[]); []) ;
+    mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
     mind_nparams = mib.mind_nparams;
     mind_nparams_rec = mib.mind_nparams_rec;
     mind_params_ctxt =
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 301c3b152..20436cbe7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -49,8 +49,9 @@ let named_context_val env = env.env_named_context,env.env_named_vals
 let rel_context env = env.env_rel_context
 
 let empty_context env =
-  env.env_rel_context = empty_rel_context
-  && env.env_named_context = empty_named_context
+  match env.env_rel_context, env.env_named_context with
+  | [], [] -> true
+  | _ -> false
 
 (* Rel context *)
 let lookup_rel n env =
@@ -321,7 +322,7 @@ let apply_to_hyp (ctxt,vals) id f =
   let rec aux rtail ctxt vals =
     match ctxt, vals with
     | (idc,c,ct as d)::ctxt, v::vals ->
-	if idc = id then
+	if id_eq idc id then
 	  (f ctxt d rtail)::ctxt, v::vals
 	else
 	  let ctxt',vals' = aux (d::rtail) ctxt vals in
@@ -334,7 +335,7 @@ let apply_to_hyp_and_dependent_on (ctxt,vals) id f g =
   let rec aux ctxt vals =
     match ctxt,vals with
     | (idc,c,ct as d)::ctxt, v::vals ->
-	if idc = id then
+	if id_eq idc id then
 	  let sign = ctxt,vals in
 	  push_named_context_val (f d sign) sign
 	else
@@ -348,7 +349,7 @@ let insert_after_hyp (ctxt,vals) id d check =
   let rec aux ctxt vals =
     match  ctxt, vals with
     | (idc,c,ct)::ctxt', v::vals' ->
-	if idc = id then begin
+	if id_eq idc id then begin
 	  check ctxt;
 	  push_named_context_val d (ctxt,vals)
 	end else
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index 30c2387ea..319f95c61 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -49,7 +49,7 @@ let rec reloc_rel n = function
 
 let rec is_lift_id = function
   | ELID -> true
-  | ELSHFT(e,n) -> n=0 & is_lift_id e
+  | ELSHFT(e,n) -> Int.equal n 0 & is_lift_id e
   | ELLFT (_,e) -> is_lift_id e
 
 (*********************)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c53a0bcd9..a44afce2b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -190,7 +190,7 @@ let type_of_inductive_knowing_parameters ?(polyprop=true) env mip paramtyps =
       (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
          the situation where a non-Prop singleton inductive becomes Prop
          when applied to Prop params *)
-      if not polyprop && not (is_type0m_univ ar.poly_level) && s = prop_sort
+      if not polyprop && not (is_type0m_univ ar.poly_level) && is_prop_sort s
       then raise (SingletonInductiveBecomesProp mip.mind_typename);
       mkArity (List.rev ctx,s)
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f2511dbde..a85395497 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -31,6 +31,8 @@ type delta_hint =
 module Deltamap = struct
   type t = module_path MPmap.t * delta_hint KNmap.t
   let empty = MPmap.empty, KNmap.empty
+  let is_empty (mm, km) =
+    MPmap.is_empty mm && KNmap.is_empty km
   let add_kn kn hint (mm,km) = (mm,KNmap.add kn hint km)
   let add_mp mp mp' (mm,km) = (MPmap.add mp mp' mm, km)
   let find_mp mp map = MPmap.find mp (fst map)
@@ -391,10 +393,10 @@ let subst_mps sub c =
 
 let rec replace_mp_in_mp mpfrom mpto mp =
   match mp with
-    | _ when mp = mpfrom -> mpto
+    | _ when mp_eq mp mpfrom -> mpto
     | MPdot (mp1,l) ->
 	let mp1' = replace_mp_in_mp mpfrom mpto mp1 in
-	  if mp1==mp1' then mp
+	  if mp1 == mp1' then mp
 	  else MPdot (mp1',l)
     | _ -> mp
 
@@ -406,7 +408,7 @@ let replace_mp_in_kn mpfrom mpto kn =
 
 let rec mp_in_mp mp mp1 =
   match mp1 with
-    | _ when mp1 = mp -> true
+    | _ when mp_eq mp1 mp -> true
     | MPdot (mp2,l) -> mp_in_mp mp mp2
     | _ -> false
 
@@ -483,7 +485,7 @@ let update_delta_resolver resolver1 resolver2 =
 let add_delta_resolver resolver1 resolver2 =
   if resolver1 == resolver2 then
     resolver2
-  else if resolver2 = empty_delta_resolver then
+  else if Deltamap.is_empty resolver2 then
     resolver1
   else
     Deltamap.join (update_delta_resolver resolver1 resolver2) resolver2
@@ -522,13 +524,13 @@ let join subst1 subst2 =
   Umap.join subst2 subst
 
 let rec occur_in_path mbi = function
-  | MPbound bid' -> mbi = bid'
+  | MPbound bid' -> mod_bound_id_eq mbi bid'
   | MPdot (mp1,_) -> occur_in_path mbi mp1
   | _ -> false
 
 let occur_mbid mbi sub =
   let check_one mbi' (mp,_) =
-    if mbi = mbi' || occur_in_path mbi mp then raise Exit
+    if mod_bound_id_eq mbi mbi' || occur_in_path mbi mp then raise Exit
   in
   try
     Umap.iter_mbi check_one sub;
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 1bef6bf50..084628a4e 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -138,10 +138,10 @@ let module_body_of_type mp mtb =
     mod_retroknowledge = []}
 
 let check_modpath_equiv env mp1 mp2 = 
-  if mp1=mp2 then () else
+  if mp_eq mp1 mp2 then () else
     let mb1=lookup_module  mp1 env in
     let mb2=lookup_module mp2 env in
-      if (mp_of_delta mb1.mod_delta mp1)=(mp_of_delta mb2.mod_delta mp2)
+      if mp_eq (mp_of_delta mb1.mod_delta mp1) (mp_of_delta mb2.mod_delta mp2)
       then ()
       else error_not_equal_modpaths mp1 mp2
 	
@@ -184,7 +184,7 @@ and subst_structure sub do_delta sign =
 
 and subst_module sub do_delta mb =
   let mp = subst_mp sub mb.mod_mp in
-  let sub = if is_functor mb.mod_type && not(mp=mb.mod_mp) then
+  let sub = if is_functor mb.mod_type && not (mp_eq mp mb.mod_mp) then
     add_mp mb.mod_mp mp
       empty_delta_resolver sub else sub in 
   let id_delta = (fun x y-> x) in
@@ -557,7 +557,7 @@ and clean_expr l = function
  | SEBfunctor (mbid,sigt,str) as s->
      let str_clean = clean_expr l str in
      let sig_clean = clean_expr l sigt.typ_expr in 
-       if  str_clean == str && sig_clean = sigt.typ_expr then
+       if  str_clean == str && Int.equal (Pervasives.compare sig_clean sigt.typ_expr) 0 then (** FIXME **)
 	 s else SEBfunctor (mbid,{sigt with typ_expr=sig_clean},str_clean)
   | SEBstruct str as s->
       let str_clean = Util.List.smartmap (clean_struct l) str in 
diff --git a/kernel/names.ml b/kernel/names.ml
index 250b4a6b5..08b111cd6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -42,9 +42,9 @@ let id_of_string s =
 
 let string_of_id id = String.copy id
 
-let id_ord (x : string) (y : string) =
-  (* String.compare already checks for pointer equality *)
-  String.compare x y
+let id_ord = String.compare
+
+let id_eq = String.equal
 
 module IdOrdered =
   struct
@@ -69,6 +69,11 @@ module Idpred = Predicate.Make(IdOrdered)
 type name = Name of identifier | Anonymous
 type variable = identifier
 
+let name_eq n1 n2 = match n1, n2 with
+| Anonymous, Anonymous -> true
+| Name id1, Name id2 -> String.equal id1 id2
+| _ -> false
+
 (** {6 Directory paths = section names paths } *)
 
 (** Dirpaths are lists of module identifiers.
@@ -134,6 +139,7 @@ module Umap = Map.Make(UOrdered)
 
 type mod_bound_id = uniq_ident
 let mod_bound_id_ord = uniq_ident_ord
+let mod_bound_id_eq mbl mbr = Int.equal (uniq_ident_ord mbl mbr) 0
 let make_mbid = make_uid
 let repr_mbid (n, id, dp) = (n, id, dp)
 let debug_string_of_mbid = debug_string_of_uid
@@ -187,6 +193,8 @@ let rec mp_ord mp1 mp2 =
   | MPbound _, MPdot _ -> -1
   | MPdot _, _ -> 1
 
+let mp_eq mp1 mp2 = Int.equal (mp_ord mp1 mp2) 0
+
 module MPord = struct
   type t = module_path
   let compare = mp_ord
@@ -214,7 +222,9 @@ let label kn =
   let _,_,l = repr_kn kn in l
 
 let string_of_kn (mp,dir,l) =
-  let str_dir = if dir = [] then "." else "#" ^ string_of_dirpath dir ^ "#"
+  let str_dir = match dir with
+  | [] -> "."
+  | _ -> "#" ^ string_of_dirpath dir ^ "#"
   in
   string_of_mp mp ^ str_dir ^ string_of_label l
 
@@ -380,9 +390,10 @@ type evaluable_global_reference =
   | EvalVarRef of identifier
   | EvalConstRef of constant
 
-let eq_egr e1 e2 = match e1,e2 with
+let eq_egr e1 e2 = match e1, e2 with
     EvalConstRef con1, EvalConstRef con2 -> eq_constant con1 con2
-  | _,_ -> e1 = e2
+  | EvalVarRef id1, EvalVarRef id2 -> Int.equal (id_ord id1 id2) 0
+  | _, _ -> false
 
 (** {6 Hash-consing of name objects } *)
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 5c2bd5b0a..5ab3b5c3f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -18,6 +18,7 @@ val string_of_id : identifier -> string
 val id_of_string : string -> identifier
 
 val id_ord : identifier -> identifier -> int
+val id_eq : identifier -> identifier -> bool
 
 (** Identifiers sets and maps *)
 module Idset  : Set.S with type elt = identifier
@@ -33,6 +34,8 @@ end
 type name = Name of identifier | Anonymous
 type variable = identifier
 
+val name_eq : name -> name -> bool
+
 (** {6 Directory paths = section names paths } *)
 
 type module_ident = identifier
@@ -71,6 +74,7 @@ module Labmap : Map.S with type key = label
 type mod_bound_id
 
 val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int
+val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool
 
 (** The first argument is a file name - to prevent conflict between
    different files *)
@@ -88,6 +92,9 @@ type module_path =
   | MPbound of mod_bound_id
   | MPdot of module_path * label
 
+val mp_ord : module_path -> module_path -> int
+val mp_eq : module_path -> module_path -> bool
+
 val check_bound_mp : module_path -> bool
 
 val string_of_mp : module_path -> string
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 6e5a45b9c..207a37f97 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -116,7 +116,7 @@ let push_named d env =
       env_named_vals =  (id,rval):: env.env_named_vals }
 
 let lookup_named_val id env =
-  snd(List.find (fun (id',_) -> id = id') env.env_named_vals)
+  snd(List.find (fun (id',_) -> id_eq id id') env.env_named_vals)
 
 (* Warning all the names should be different *)
 let env_of_named id env = env
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1d974eada..b0ea2f7db 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -51,15 +51,15 @@ let el_stack el stk =
 let compare_stack_shape stk1 stk2 =
   let rec compare_rec bal stk1 stk2 =
   match (stk1,stk2) with
-      ([],[]) -> bal=0
+      ([],[]) -> Int.equal bal 0
     | ((Zupdate _|Zshift _)::s1, _) -> compare_rec bal s1 stk2
     | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
     | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
     | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
     | (Zcase(c1,_,_)::s1, Zcase(c2,_,_)::s2) ->
-        bal=0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
+        Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
     | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
-        bal=0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
+        Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
     | (_,_) -> false in
   compare_rec 0 stk1 stk2
 
@@ -181,14 +181,18 @@ type conv_pb =
   | CONV
   | CUMUL
 
+let is_cumul = function CUMUL -> true | CONV -> false
+
 let sort_cmp pb s0 s1 cuniv =
   match (s0,s1) with
-    | (Prop c1, Prop c2) when pb = CUMUL ->
-        if c1 = Null or c2 = Pos then cuniv   (* Prop <= Set *)
-        else raise NotConvertible
+    | (Prop c1, Prop c2) when is_cumul pb ->
+      begin match c1, c2 with
+      | Null, _ | _, Pos -> cuniv (* Prop <= Set *)
+      | _ -> raise NotConvertible
+      end
     | (Prop c1, Prop c2) ->
-        if c1 = c2 then cuniv else raise NotConvertible
-    | (Prop c1, Type u) when pb = CUMUL -> assert (is_univ_variable u); cuniv
+        if c1 == c2 then cuniv else raise NotConvertible
+    | (Prop c1, Type u) when is_cumul pb -> assert (is_univ_variable u); cuniv
     | (Type u1, Type u2) ->
 	assert (is_univ_variable u2);
 	(match pb with
@@ -266,12 +270,12 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 		 anomaly "conversion was given ill-typed terms (Sort)";
 	       sort_cmp cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
-               if n=m
+               if Int.equal n m
 	       then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
                else raise NotConvertible
 	   | _ -> raise NotConvertible)
     | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
-        if ev1=ev2 then
+        if Int.equal ev1 ev2 then
           let u1 = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
           convert_vect l2r infos el1 el2
             (Array.map (mk_clos env1) args1)
@@ -280,7 +284,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     (* 2 index known to be bound to no constant *)
     | (FRel n, FRel m) ->
-        if reloc_rel n el1 = reloc_rel m el2
+        if Int.equal (reloc_rel n el1) (reloc_rel m el2)
         then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
@@ -362,13 +366,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         else raise NotConvertible
 
     | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
-	if j1 = j2 && eq_ind ind1 ind2
+	if Int.equal j1 j2 && eq_ind ind1 ind2
 	then
           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
-    | (FFix ((op1,(_,tys1,cl1)),e1), FFix((op2,(_,tys2,cl2)),e2)) ->
-	if op1 = op2
+    | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) ->
+	if Int.equal i1 i2 && Array.equal Int.equal op1 op2
 	then
 	  let n = Array.length cl1 in
           let fty1 = Array.map (mk_clos e1) tys1 in
@@ -383,7 +387,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
         else raise NotConvertible
 
     | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
-        if op1 = op2
+        if Int.equal op1 op2
         then
 	  let n = Array.length cl1 in
           let fty1 = Array.map (mk_clos e1) tys1 in
@@ -414,7 +418,7 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
 and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
   let lv1 = Array.length v1 in
   let lv2 = Array.length v2 in
-  if lv1 = lv2
+  if Int.equal lv1 lv2
   then
     let rec fold n univ =
       if n >= lv1 then univ
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 269f7a5d9..b2a509678 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -29,7 +29,7 @@ let empty_named_context = []
 let add_named_decl d sign = d::sign
 
 let rec lookup_named id = function
-  | (id',_,_ as decl) :: _ when id=id' -> decl
+  | (id',_,_ as decl) :: _ when id_eq id id' -> decl
   | _ :: sign -> lookup_named id sign
   | [] -> raise Not_found
 
diff --git a/kernel/term.ml b/kernel/term.ml
index a99262adf..94aa7d968 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -63,6 +63,10 @@ let prop_sort = Prop Null
 let set_sort = Prop Pos
 let type1_sort = Type type1_univ
 
+let is_prop_sort = function
+| Prop Null -> true
+| _ -> false
+
 type sorts_family = InProp | InSet | InType
 
 let family_of_sort = function
@@ -138,7 +142,7 @@ let mkSort   = function
 (* (that means t2 is declared as the type of t1) *)
 let mkCast (t1,k2,t2) =
   match t1 with
-  | Cast (c,k1, _) when k1 = VMcast & k1 = k2 -> Cast (c,k1,t2)
+  | Cast (c,k1, _) when k1 == VMcast && k1 == k2 -> Cast (c,k1,t2)
   | _ -> Cast (t1,k2,t2)
 
 (* Constructs the product (x:t1)t2 *)
@@ -265,7 +269,7 @@ let destMeta c = match kind_of_term c with
   | _ -> invalid_arg "destMeta"
 
 let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false
-let isMetaOf mv c = match kind_of_term c with Meta mv' -> mv = mv' | _ -> false
+let isMetaOf mv c = match kind_of_term c with Meta mv' -> Int.equal mv mv' | _ -> false
 
 (* Destructs a variable *)
 let destVar c = match kind_of_term c with
@@ -324,11 +328,11 @@ let isCast c = match kind_of_term c with Cast _ -> true | _ -> false
 
 (* Tests if a de Bruijn index *)
 let isRel c = match kind_of_term c with Rel _ -> true | _ -> false
-let isRelN n c = match kind_of_term c with Rel n' -> n = n' | _ -> false
+let isRelN n c = match kind_of_term c with Rel n' -> Int.equal n n' | _ -> false
 
 (* Tests if a variable *)
 let isVar c = match kind_of_term c with Var _ -> true | _ -> false
-let isVarId id c = match kind_of_term c with Var id' -> id = id' | _ -> false
+let isVarId id c = match kind_of_term c with Var id' -> Int.equal (id_ord id id') 0 | _ -> false
 
 (* Tests if an inductive *)
 let isInd c = match kind_of_term c with Ind _ -> true | _ -> false
@@ -559,30 +563,31 @@ let map_constr_with_binders g f l c = match kind_of_term c with
 
 let compare_constr f t1 t2 =
   match kind_of_term t1, kind_of_term t2 with
-  | Rel n1, Rel n2 -> n1 = n2
-  | Meta m1, Meta m2 -> m1 = m2
-  | Var id1, Var id2 -> id1 = id2
-  | Sort s1, Sort s2 -> s1 = s2
+  | Rel n1, Rel n2 -> Int.equal n1 n2
+  | Meta m1, Meta m2 -> Int.equal m1 m2
+  | Var id1, Var id2 -> Int.equal (id_ord id1 id2) 0
+  | Sort s1, Sort s2 -> Int.equal (Pervasives.compare s1 s2) 0 (** FIXME **)
   | Cast (c1,_,_), _ -> f c1 t2
   | _, Cast (c2,_,_) -> f t1 c2
-  | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 & f c1 c2
-  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 & f c1 c2
-  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
+  | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
+  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 && f c1 c2
+  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 && f t1 t2 && f c1 c2
   | App (c1,l1), _ when isCast c1 -> f (mkApp (pi1 (destCast c1),l1)) t2
   | _, App (c2,l2) when isCast c2 -> f t1 (mkApp (pi1 (destCast c2),l2))
   | App (c1,l1), App (c2,l2) ->
-    Array.length l1 = Array.length l2 &&
-      f c1 c2 && Array.for_all2 f l1 l2
-  | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & Array.for_all2 f l1 l2
+    Int.equal (Array.length l1) (Array.length l2) &&
+      f c1 c2 && Array.equal f l1 l2
+  | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2
   | Const c1, Const c2 -> eq_constant c1 c2
   | Ind c1, Ind c2 -> eq_ind c1 c2
   | Construct c1, Construct c2 -> eq_constructor c1 c2
   | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-      f p1 p2 & f c1 c2 & Array.for_all2 f bl1 bl2
-  | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
-      ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2
+      f p1 p2 & f c1 c2 && Array.equal f bl1 bl2
+  | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
+      Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
+      && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      ln1 = ln2 & Array.for_all2 f tl1 tl2 & Array.for_all2 f bl1 bl2
+      Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
   | _ -> false
 
 (*******************************)
@@ -592,21 +597,20 @@ let compare_constr f t1 t2 =
 (* alpha conversion : ignore print names and casts *)
 
 let rec eq_constr m n =
-  (m==n) or
-  compare_constr eq_constr m n
+  (m == n) || compare_constr eq_constr m n
 
 let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
 let constr_ord_int f t1 t2 =
   let (=?) f g i1 i2 j1 j2=
-    let c=f i1 i2 in
-    if c=0 then g j1 j2 else c in
+    let c = f i1 i2 in
+    if Int.equal c 0 then g j1 j2 else c in
   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 in
+    if Int.equal c 0 then h k1 k2 else c in
   match kind_of_term t1, kind_of_term t2 with
-    | Rel n1, Rel n2 -> n1 - n2
-    | Meta m1, Meta m2 -> m1 - m2
+    | Rel n1, Rel n2 -> Int.compare n1 n2
+    | Meta m1, Meta m2 -> Int.compare m1 m2
     | Var id1, Var id2 -> id_ord id1 id2
     | Sort s1, Sort s2 -> Pervasives.compare s1 s2
     | Cast (c1,_,_), _ -> f c1 t2
@@ -671,7 +675,7 @@ let eq_named_declaration (i1, c1, t1) (i2, c2, t2) =
   Int.equal (id_ord i1 i2) 0 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
 
 let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
-  n1 = n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
+  name_eq n1 n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
 
 (***************************************************************************)
 (*     Type of local contexts (telescopes)                                 *)
@@ -729,7 +733,7 @@ let closed0 = closedn 0
 
 let noccurn n term =
   let rec occur_rec n c = match kind_of_term c with
-    | Rel m -> if m = n then raise LocalOccur
+    | Rel m -> if Int.equal m n then raise LocalOccur
     | _ -> iter_constr_with_binders succ occur_rec n c
   in
   try occur_rec n term; true with LocalOccur -> false
@@ -839,7 +843,7 @@ let subst1_named_decl = subst1_decl
 let rec thin_val = function
   | [] -> []
   | (((id,{ sit = v }) as s)::tl) when isVar v ->
-      if id = destVar v then thin_val tl else s::(thin_val tl)
+      if Int.equal (id_ord id (destVar v)) 0 then thin_val tl else s::(thin_val tl)
   | h::tl -> h::(thin_val tl)
 
 (* (replace_vars sigma M) applies substitution sigma to term M *)
@@ -853,7 +857,9 @@ let replace_vars var_alist =
          with Not_found -> c)
     | _ -> map_constr_with_binders succ substrec n c
   in
-  if var_alist = [] then (function x -> x) else substrec 0
+  match var_alist with
+  | [] -> (function x -> x)
+  | _ -> substrec 0
 
 (*
 let repvarkey = Profile.declare_profile "replace_vars";;
@@ -1017,7 +1023,7 @@ let decompose_lam =
 let decompose_prod_n n =
   if n < 0 then error "decompose_prod_n: integer parameter must be positive";
   let rec prodec_rec l n c =
-    if n=0 then l,c
+    if Int.equal n 0 then l,c
     else match kind_of_term c with
       | Prod (x,t,c) -> prodec_rec ((x,t)::l) (n-1) c
       | Cast (c,_,_)   -> prodec_rec l n c
@@ -1030,7 +1036,7 @@ let decompose_prod_n n =
 let decompose_lam_n n =
   if n < 0 then error "decompose_lam_n: integer parameter must be positive";
   let rec lamdec_rec l n c =
-    if n=0 then l,c
+    if Int.equal n 0 then l,c
     else match kind_of_term c with
       | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
       | Cast (c,_,_)     -> lamdec_rec l n c
@@ -1068,7 +1074,7 @@ let decompose_prod_n_assum n =
   if n < 0 then
     error "decompose_prod_n_assum: integer parameter must be positive";
   let rec prodec_rec l n c =
-    if n=0 then l,c
+    if Int.equal n 0 then l,c
     else match kind_of_term c with
     | Prod (x,t,c)    -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c
     | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
@@ -1085,7 +1091,7 @@ let decompose_lam_n_assum n =
   if n < 0 then
     error "decompose_lam_n_assum: integer parameter must be positive";
   let rec lamdec_rec l n c =
-    if n=0 then l,c
+    if Int.equal n 0 then l,c
     else match kind_of_term c with
     | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
     | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c
@@ -1199,9 +1205,9 @@ let rec isArity c =
 
 let array_eqeq t1 t2 =
   t1 == t2 ||
-  (Array.length t1 = Array.length t2 &&
+  (Int.equal (Array.length t1) (Array.length t2) &&
    let rec aux i =
-     (i = Array.length t1) || (t1.(i) == t2.(i) && aux (i + 1))
+     (Int.equal i (Array.length t1)) || (t1.(i) == t2.(i) && aux (i + 1))
    in aux 0)
 
 let equals_constr t1 t2 =
@@ -1216,20 +1222,21 @@ let equals_constr t1 t2 =
     | LetIn (n1,b1,t1,c1), LetIn (n2,b2,t2,c2) ->
       n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2
     | App (c1,l1), App (c2,l2) -> c1 == c2 & array_eqeq l1 l2
-    | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_eqeq l1 l2
+    | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 & array_eqeq l1 l2
     | Const c1, Const c2 -> c1 == c2
-    | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 & i1 = i2
+    | Ind (sp1,i1), Ind (sp2,i2) -> sp1 == sp2 && Int.equal i1 i2
     | Construct ((sp1,i1),j1), Construct ((sp2,i2),j2) ->
-      sp1 == sp2 & i1 = i2 & j1 = j2
+      sp1 == sp2 && Int.equal i1 i2 && Int.equal j1 j2
     | Case (ci1,p1,c1,bl1), Case (ci2,p2,c2,bl2) ->
       ci1 == ci2 & p1 == p2 & c1 == c2 & array_eqeq bl1 bl2
-    | Fix (ln1,(lna1,tl1,bl1)), Fix (ln2,(lna2,tl2,bl2)) ->
-      ln1 = ln2
-      & array_eqeq lna1 lna2
-      & array_eqeq tl1 tl2
-      & array_eqeq bl1 bl2
+    | Fix ((ln1, i1),(lna1,tl1,bl1)), Fix ((ln2, i2),(lna2,tl2,bl2)) ->
+      Int.equal i1 i2
+      && Array.equal Int.equal ln1 ln2
+      && array_eqeq lna1 lna2
+      && array_eqeq tl1 tl2
+      && array_eqeq bl1 bl2
     | CoFix(ln1,(lna1,tl1,bl1)), CoFix(ln2,(lna2,tl2,bl2)) ->
-      ln1 = ln2
+      Int.equal ln1 ln2
       & array_eqeq lna1 lna2
       & array_eqeq tl1 tl2
       & array_eqeq bl1 bl2
@@ -1379,7 +1386,7 @@ module Hsorts =
         | Type u -> Type (huniv u)
       let equal s1 s2 =
         match (s1,s2) with
-            (Prop c1, Prop c2) -> c1=c2
+            (Prop c1, Prop c2) -> c1 == c2
           | (Type u1, Type u2) -> u1 == u2
           |_ -> false
       let hash = Hashtbl.hash
@@ -1391,11 +1398,14 @@ module Hcaseinfo =
       type t = case_info
       type u = inductive -> inductive
       let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
+      let pp_info_equal info1 info2 =
+        Int.equal info1.ind_nargs info2.ind_nargs &&
+        info1.style == info2.style
       let equal ci ci' =
 	ci.ci_ind == ci'.ci_ind &&
-	ci.ci_npar = ci'.ci_npar &&
-	ci.ci_cstr_ndecls = ci'.ci_cstr_ndecls && (* we use (=) on purpose *)
-	ci.ci_pp_info = ci'.ci_pp_info  (* we use (=) on purpose *)
+	Int.equal ci.ci_npar ci'.ci_npar &&
+	Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
+	pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
       let hash = Hashtbl.hash
     end)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 15fcdd189..85192e1f1 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -21,6 +21,8 @@ val set_sort  : sorts
 val prop_sort : sorts
 val type1_sort  : sorts
 
+val is_prop_sort : sorts -> bool
+
 (** {6 The sorts family of CCI. } *)
 
 type sorts_family = InProp | InSet | InType
diff --git a/kernel/univ.ml b/kernel/univ.ml
index bdd668cbd..18bee0fb4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -557,7 +557,7 @@ type constraint_function =
 
 let constraint_add_leq v u c =
   (* We just discard trivial constraints like Set<=u or u<=u *)
-  if v = UniverseLevel.Set || UniverseLevel.equal v u then c
+  if UniverseLevel.equal v UniverseLevel.Set || UniverseLevel.equal v u then c
   else Constraint.add (v,Le,u) c
 
 let enforce_leq u v c =
@@ -634,12 +634,16 @@ let normalize_universes g =
 let check_sorted g sorted =
   let get u = try UniverseLMap.find u sorted with
     | Not_found -> assert false
-  in UniverseLMap.iter (fun u arc -> let lu = get u in match arc with
-    | Equiv v -> assert (lu = get v)
-    | Canonical {univ=u'; lt=lt; le=le} ->
+  in
+  let iter u arc =
+    let lu = get u in match arc with
+    | Equiv v -> assert (Int.equal lu (get v))
+    | Canonical {univ = u'; lt = lt; le = le} ->
       assert (u == u');
       List.iter (fun v -> assert (lu <= get v)) le;
-      List.iter (fun v -> assert (lu < get v)) lt) g
+      List.iter (fun v -> assert (lu < get v)) lt
+  in
+  UniverseLMap.iter iter g
 
 (**
   Bellman-Ford algorithm with a few customizations:
@@ -648,7 +652,10 @@ let check_sorted g sorted =
       vertices, and [bottom] is used as the source vertex
 *)
 let bellman_ford bottom g =
-  assert (lookup_level bottom g = None);
+  let () = match lookup_level bottom g with
+  | None -> ()
+  | Some _ -> assert false
+  in
   let ( << ) a b = match a, b with
     | _, None -> true
     | None, _ -> false
@@ -790,11 +797,11 @@ let make_max = function
   | (le,lt) -> Max (le,lt)
 
 let remove_large_constraint u = function
-  | Atom u' as x -> if u = u' then Max ([],[]) else x
+  | Atom u' as x -> if UniverseLevel.equal u u' then Max ([],[]) else x
   | Max (le,lt) -> make_max (List.remove u le,lt)
 
 let is_direct_constraint u = function
-  | Atom u' -> u = u'
+  | Atom u' -> UniverseLevel.equal u u'
   | Max (le,lt) -> List.mem u le
 
 (*
@@ -854,7 +861,7 @@ let no_upper_constraints u cst =
 
 let univ_depends u v =
   match u, v with
-    | Atom u, Atom v -> u = v
+    | Atom u, Atom v -> UniverseLevel.equal u v
     | Atom u, Max (gel,gtl) -> List.mem u gel || List.mem u gtl
     | _ -> anomaly "univ_depends given a non-atomic 1st arg"
 
@@ -948,7 +955,7 @@ module Hconstraint =
       type u = universe_level -> universe_level
       let hashcons hul (l1,k,l2) = (hul l1, k, hul l2)
       let equal (l1,k,l2) (l1',k',l2') =
-	l1 == l1' && k = k' && l2 == l2'
+	l1 == l1' && k == k' && l2 == l2'
       let hash = Hashtbl.hash
     end)