Monomorphization (kernel)

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

16 files changed, 192 insertions, 126 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 1c9b2145d..14b2a3a6e 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -692,7 +692,7 @@ let fapp_stack (m,stk) = zip m stk
 
 (* optimised for the case where there are no shifts... *)
 let strip_update_shift_app head stk =
-  assert (head.norm <> Red);
+  assert (match head.norm with Red -> false | _ -> true);
   let rec strip_rec rstk h depth = function
     | Zshift(k) as e :: s ->
         strip_rec (e::rstk) (lift_fconstr k h) (depth+k) s
@@ -706,7 +706,7 @@ let strip_update_shift_app head stk =
 
 
 let get_nth_arg head n stk =
-  assert (head.norm <> Red);
+  assert (match head.norm with Red -> false | _ -> true);
   let rec strip_rec rstk h n = function
     | Zshift(k) as e :: s ->
         strip_rec (e::rstk) (lift_fconstr k h) n s
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f016a20b7..99b582fe3 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -75,6 +75,9 @@ let update_case_info ci modlist =
 
 let empty_modlist = (Cmap.empty, Mindmap.empty)
 
+let is_empty_modlist (cm, mm) =
+  Cmap.is_empty cm && Mindmap.is_empty mm
+
 let expmod_constr modlist c =
   let rec substrec c =
     match kind_of_term c with
@@ -102,7 +105,7 @@ let expmod_constr modlist c =
   | _ -> map_constr substrec c
 
   in
-  if modlist = empty_modlist then c
+  if is_empty_modlist modlist then c
   else substrec c
 
 let abstract_constant_type =
@@ -136,7 +139,7 @@ let cook_constant env r =
   in
   let const_hyps =
     Sign.fold_named_context (fun (h,_,_) hyps ->
-      List.filter (fun (id,_,_) -> id <> h) hyps)
+      List.filter (fun (id,_,_) -> not (id_eq id h)) hyps)
       hyps ~init:cb.const_hyps in
   let typ = match cb.const_type with
     | NonPolymorphicType t ->
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index b995f2e4a..3e5b10f3b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -180,6 +180,12 @@ type recarg =
   | Mrec of inductive
   | Imbr of inductive
 
+let eq_recarg r1 r2 = match r1, r2 with
+| Norec, Norec -> true
+| Mrec i1, Mrec i2 -> eq_ind i1 i2
+| Imbr i1, Imbr i2 -> eq_ind i1 i2
+| _ -> false
+
 let subst_recarg sub r = match r with
   | Norec -> r
   | Mrec (kn,i) -> let kn' = subst_ind sub kn in
@@ -204,7 +210,7 @@ let dest_recarg p = fst (Rtree.dest_node p)
  *)
 let dest_subterms p =
   let (ra,cstrs) = Rtree.dest_node p in
-  assert (ra<>Norec);
+  assert (match ra with Norec -> false | _ -> true);
   Array.map (fun t -> Array.to_list (snd (Rtree.dest_node t))) cstrs
 
 let recarg_length p j =
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index a298d56ae..0a09ad76f 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -89,6 +89,8 @@ type recarg =
   | Mrec of inductive
   | Imbr of inductive
 
+val eq_recarg : recarg -> recarg -> bool
+
 val subst_recarg : substitution -> recarg -> recarg
 
 type wf_paths = recarg Rtree.t
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6b993604d..042961879 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -90,7 +90,7 @@ let mind_check_names mie =
 
 (* Typing the arities and constructor types *)
 
-let is_logic_type t = (t.utj_type = prop_sort)
+let is_logic_type t = is_prop_sort t.utj_type
 
 (* [infos] is a sequence of pair [islogic,issmall] for each type in
    the product of a constructor or arity *)
@@ -179,7 +179,10 @@ let infer_constructor_packet env_ar_par params lc =
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
 let typecheck_inductive env mie =
-  if mie.mind_entry_inds = [] then anomaly "empty inductive types declaration";
+  let () = match mie.mind_entry_inds with
+  | [] -> anomaly "empty inductive types declaration"
+  | _ -> ()
+  in
   (* Check unicity of names *)
   mind_check_names mie;
   (* Params are typed-checked here *)
@@ -233,22 +236,25 @@ let typecheck_inductive env mie =
 
   let inds = Array.of_list inds in
   let arities = Array.of_list arity_list in
-  let param_ccls = List.fold_left (fun l (_,b,p) ->
-    if b = None then
-      (* Parameter contributes to polymorphism only if explicit Type *)
-      let c = strip_prod_assum p in
-      (* Add Type levels to the ordered list of parameters contributing to *)
-      (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
-      match kind_of_term c with
-      | Sort (Type u) ->
-          if List.mem (Some u) l then
-            None :: List.map (function Some v when u = v -> None | x -> x) l
-          else
-            Some u :: l
-      | _ ->
-          None :: l
-    else
-      l) [] params in
+  let fold l (_, b, p) = match b with
+  | None ->
+    (* Parameter contributes to polymorphism only if explicit Type *)
+    let c = strip_prod_assum p in
+    (* Add Type levels to the ordered list of parameters contributing to *)
+    (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
+    begin match kind_of_term c with
+    | Sort (Type u) ->
+      if List.mem (Some u) l then
+        (** FIXME *)
+        None :: List.map (function Some v when Pervasives.(=) u v -> None | x -> x) l
+      else
+        Some u :: l
+    | _ ->
+      None :: l
+    end
+  | _ -> l
+  in
+  let param_ccls = List.fold_left fold [] params in
 
   (* Compute/check the sorts of the inductive types *)
   let ind_min_levels = inductive_levels arities inds in
@@ -256,7 +262,7 @@ let typecheck_inductive env mie =
     Array.fold_map2' (fun ((id,full_arity,ar_level),cn,info,lc,_) lev cst ->
       let sign, s = dest_arity env full_arity in
       let status,cst = match s with
-      | Type u when ar_level <> None (* Explicitly polymorphic *)
+      | Type u when ar_level != None (* Explicitly polymorphic *)
             && no_upper_constraints u cst ->
 	  (* The polymorphic level is a function of the level of the *)
 	  (* conclusions of the parameters *)
@@ -265,7 +271,11 @@ let typecheck_inductive env mie =
 	  Inr (param_ccls, lev), enforce_leq lev u cst
       | Type u (* Not an explicit occurrence of Type *) ->
 	  Inl (info,full_arity,s), enforce_leq lev u cst
-      | Prop Pos when engagement env <> Some ImpredicativeSet ->
+      | Prop Pos when
+        begin match engagement env with
+        | Some ImpredicativeSet -> false
+        | _ -> true
+        end ->
 	  (* Predicative set: check that the content is indeed predicative *)
 	  if not (is_type0m_univ lev) & not (is_type0_univ lev) then
 	    raise (InductiveError LargeNonPropInductiveNotInType);
@@ -337,7 +347,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     | (_,Some _,_)::hyps -> check k (index+1) hyps
     | _::hyps ->
         match kind_of_term (whd_betadeltaiota env lpar.(k)) with
-	  | Rel w when w = index -> check (k-1) (index+1) hyps
+	  | Rel w when Int.equal w index -> check (k-1) (index+1) hyps
 	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
   in check (nparams-1) (n-nhyps) hyps;
   if not (Array.for_all (noccur_between n ntypes) largs') then
@@ -359,7 +369,7 @@ if Int.equal nmr 0 then 0 else
 	| (lp,(_,Some _,_)::hyps) -> find k (index-1) (lp,hyps)
 	| (p::lp,_::hyps) ->
        ( match kind_of_term (whd_betadeltaiota env p) with
-	  | Rel w when w = index -> find (k+1) (index-1) (lp,hyps)
+	  | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,hyps)
           | _ -> k)
   in find 0 (n-1) (lpar,List.rev hyps)
 
@@ -403,7 +413,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
   (env', newidx, ntypes, ra_env')
 
 let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
-  if n=0 then (ienv,c) else
+  if Int.equal n 0 then (ienv,c) else
     let c' = whd_betadeltaiota env c in
     match kind_of_term c' with
 	Prod(na,a,b) ->
@@ -424,7 +434,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
     let x,largs = decompose_app (whd_betadeltaiota env c) in
       match kind_of_term x with
 	| Prod (na,b,d) ->
-	    assert (largs = []);
+	    let () = assert (List.is_empty largs) in
             (match weaker_noccur_between env n ntypes b with
 		None -> failwith_non_pos_list n ntypes [b]
               | Some b ->
@@ -466,7 +476,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 	failwith_non_pos_list n ntypes auxlargs;
       (* We do not deal with imbricated mutual inductive types *)
       let auxntyp = mib.mind_ntypes in
-	if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n));
+	if not (Int.equal auxntyp 1) then raise (IllFormedInd (LocalNonPos n));
 	(* The nested inductive type with parameters removed *)
 	let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in
 	  (* Extends the environment with a variable corresponding to
@@ -500,21 +510,23 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 	match kind_of_term x with
 
           | Prod (na,b,d) ->
-	      assert (largs = []);
+	      let () = assert (List.is_empty largs) in
               let nmr',recarg = check_pos ienv nmr b in
               let ienv' = ienv_push_var ienv (na,b,mk_norec) in
-		check_constr_rec ienv' nmr' (recarg::lrec) d
-
-	  | hd ->
-	      if check_head then
-		if hd = Rel (n+ntypes-i-1) then
-		  check_correct_par ienv hyps (ntypes-i) largs
-		else
-		  raise (IllFormedInd LocalNotConstructor)
-	      else
-		if not (List.for_all (noccur_between n ntypes) largs)
-		then failwith_non_pos_list n ntypes largs;
-	      (nmr,List.rev lrec)
+                check_constr_rec ienv' nmr' (recarg::lrec) d
+          | hd ->
+            let () =
+              if check_head then
+                begin match hd with
+                | Rel j when Int.equal j (n + ntypes - i - 1) ->
+                  check_correct_par ienv hyps (ntypes - i) largs
+                | _ -> raise (IllFormedInd LocalNotConstructor)
+                end
+              else
+                if not (List.for_all (noccur_between n ntypes) largs)
+                then failwith_non_pos_list n ntypes largs
+            in
+            (nmr, List.rev lrec)
     in check_constr_rec ienv nmr [] c
   in
   let irecargs_nmr =
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a44afce2b..d1cffe867 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -75,7 +75,7 @@ let instantiate_params full t args sign =
       sign
       ~init:(args,[],t)
   in
-  if rem_args <> [] then fail();
+  let () = if not (List.is_empty rem_args) then fail () in
   substl subs ty
 
 let full_inductive_instantiate mib params sign =
@@ -282,7 +282,10 @@ let build_dependent_inductive ind (_,mip) params =
 exception LocalArity of (sorts_family * sorts_family * arity_error) option
 
 let check_allowed_sort ksort specif =
-  if not (List.exists ((=) ksort) (elim_sorts specif)) then
+  let eq_ksort s = match ksort, s with
+  | InProp, InProp | InSet, InSet | InType, InType -> true
+  | _ -> false in
+  if not (List.exists eq_ksort (elim_sorts specif)) then
     let s = inductive_sort_family (snd specif) in
     raise (LocalArity (Some(ksort,s,error_elim_explain ksort s)))
 
@@ -358,9 +361,9 @@ let type_case_branches env (ind,largs) pj c =
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
-    not (eq_ind indsp ci.ci_ind) or
-    (mib.mind_nparams <> ci.ci_npar) or
-    (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls)
+    not (eq_ind indsp ci.ci_ind) ||
+    not (Int.equal mib.mind_nparams ci.ci_npar) ||
+    not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
 
 (************************************************************************)
@@ -412,7 +415,7 @@ type subterm_spec =
   | Not_subterm
 
 let spec_of_tree t = lazy
-  (if Rtree.eq_rtree (=) (Lazy.force t) mk_norec
+  (if Rtree.eq_rtree eq_recarg (Lazy.force t) mk_norec
    then Not_subterm
    else Subterm(Strict,Lazy.force t))
 
@@ -424,7 +427,7 @@ let subterm_spec_glb =
       | Not_subterm, _ -> Not_subterm
       | _, Not_subterm -> Not_subterm
       | Subterm (a1,t1), Subterm (a2,t2) ->
-          if Rtree.eq_rtree (=) t1 t2 then Subterm (size_glb a1 a2, t1)
+          if Rtree.eq_rtree eq_recarg t1 t2 then Subterm (size_glb a1 a2, t1)
           (* branches do not return objects with same spec *)
           else Not_subterm in
   Array.fold_left glb2 Dead_code
@@ -515,7 +518,7 @@ let branches_specif renv c_spec ci =
 	   (match Lazy.force c_spec with
 		Subterm (_,t) when match_inductive ci.ci_ind (dest_recarg t) ->
 		  let vra = Array.of_list (dest_subterms t).(i) in
-		  assert (nca = Array.length vra);
+		  assert (Int.equal nca (Array.length vra));
 		  Array.map
 		    (fun t -> Lazy.force (spec_of_tree (lazy t)))
 		    vra
@@ -586,7 +589,7 @@ let rec subterm_specif renv stack t =
 		     subterm_specif renv'' [] strippedBody)
 
       | Lambda (x,a,b) ->
-          assert (l=[]);
+          let () = assert (List.is_empty l) in
 	  let spec,stack' = extract_stack renv a stack in
 	    subterm_specif (push_var renv (x,a,spec)) stack' b
 
@@ -711,7 +714,7 @@ let check_one_fix renv recpos def =
 	    let stack' = push_stack_closures renv l stack in
               Array.iteri
                 (fun j body ->
-                   if i=j && (List.length stack' > decrArg) then
+                   if Int.equal i j && (List.length stack' > decrArg) then
 		     let recArg = List.nth stack' decrArg in
 	             let arg_sp = stack_element_specif recArg in
 	             check_nested_fix_body renv' (decrArg+1) arg_sp body
@@ -727,13 +730,13 @@ let check_one_fix renv recpos def =
 	    else List.iter (check_rec_call renv []) l
 
         | Lambda (x,a,b) ->
-	    assert (l = []);
+            let () = assert (List.is_empty l) in
 	    check_rec_call renv [] a ;
 	    let spec, stack' = extract_stack renv a stack in
 	    check_rec_call (push_var renv (x,a,spec)) stack' b
 
         | Prod (x,a,b) ->
-	    assert (l = [] && stack = []);
+            let () = assert (List.is_empty l && List.is_empty stack) in
             check_rec_call renv [] a;
             check_rec_call (push_var_renv renv (x,a)) [] b
 
@@ -757,7 +760,8 @@ let check_one_fix renv recpos def =
 		    check_rec_call renv stack (applist(c,l))
             end
 
-	| Sort _ -> assert (l = [])
+	| Sort _ ->
+          assert (List.is_empty l)
 
         (* l is not checked because it is considered as the meta's context *)
         | (Evar _ | Meta _) -> ()
@@ -784,11 +788,11 @@ let judgment_of_fixpoint (_, types, bodies) =
 let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
   let nbfix = Array.length bodies in
   if Int.equal nbfix 0
-    or Array.length nvect <> nbfix
-    or Array.length types <> nbfix
-    or Array.length names <> nbfix
-    or bodynum < 0
-    or bodynum >= nbfix
+    || not (Int.equal (Array.length nvect) nbfix)
+    || not (Int.equal (Array.length types) nbfix)
+    || not (Int.equal (Array.length names) nbfix)
+    || bodynum < 0
+    || bodynum >= nbfix
   then anomaly "Ill-formed fix term";
   let fixenv = push_rec_types recdef env in
   let vdefj = judgment_of_fixpoint recdef in
@@ -803,7 +807,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) =
         | Lambda (x,a,b) ->
 	    if noccur_with_meta n nbfix a then
 	      let env' = push_rel (x, None, a) env in
-              if n = k+1 then
+              if Int.equal n (k + 1) then
                 (* get the inductive type of the fixpoint *)
                 let (mind, _) =
                   try find_inductive env a
@@ -873,7 +877,7 @@ let check_one_cofix env nbfix def deftype =
             let realargs = List.skipn mib.mind_nparams args in
             let rec process_args_of_constr = function
               | (t::lr), (rar::lrar) ->
-                  if rar = mk_norec then
+                  if Rtree.eq_rtree eq_recarg rar mk_norec then
                     if noccur_with_meta n nbfix t
                     then process_args_of_constr (lr, lrar)
                     else raise (CoFixGuardError
@@ -887,7 +891,7 @@ let check_one_cofix env nbfix def deftype =
             in process_args_of_constr (realargs, lra)
 
 	| Lambda (x,a,b) ->
-	     assert (args = []);
+	    let () = assert (List.is_empty args) in
             if noccur_with_meta n nbfix a then
               let env' = push_rel (x, None, a) env in
               check_rec_call env' alreadygrd (n+1)  vlra b
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index a85395497..5af6bd5bb 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -492,7 +492,7 @@ let add_delta_resolver resolver1 resolver2 =
 
 let substition_prefixed_by k mp subst =
   let mp_prefixmp kmp (mp_to,reso) sub =
-    if mp_in_mp mp kmp && mp <> kmp then
+    if mp_in_mp mp kmp && not (mp_eq mp kmp) then
       let new_key = replace_mp_in_mp mp k kmp in
       Umap.add_mp new_key (mp_to,reso) sub
     else sub
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b2312d689..b358d805a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -41,7 +41,7 @@ let is_modular = function
 
 let rec list_split_assoc ((k,m) as km) rev_before = function
   | [] -> raise Not_found
-  | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after
+  | (k',b)::after when eq_label k k' && (is_modular b) == (m : bool) -> rev_before,b,after
   | h::tail -> list_split_assoc km (h::rev_before) tail
 
 let discr_resolver env mtb =
@@ -65,11 +65,12 @@ let rec check_with env sign with_decl alg_sign mp equiv =
 	let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
 	sign,With_module_body(idl,mp1),equiv,cst
   in
-    if alg_sign = None then
-      sign,None,equiv,cst
-    else
-      sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst
-	    
+  match alg_sign with
+  | None ->
+    sign, None, equiv, cst
+  | Some s ->
+    sign,Some (SEBwith(s, wd)),equiv,cst
+
 and check_with_def env sign (idl,c) mp equiv =
   let sig_b = match sign with 
     | SEBstruct(sig_b) -> sig_b
@@ -81,10 +82,11 @@ and check_with_def env sign (idl,c) mp equiv =
   in
   let l = label_of_id id in
     try
-      let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
+      let not_empty = match idl with [] -> false | _ :: _ -> true in
+      let rev_before,spec,after = list_split_assoc (l, not_empty) [] sig_b in
       let before = List.rev rev_before in
       let env' = Modops.add_signature mp before equiv env in
-      if idl = [] then
+      match idl with [] ->
 	      (* Toplevel definition *)
 	      let cb = match spec with
 		| SFBconst cb -> cb
@@ -119,7 +121,7 @@ and check_with_def env sign (idl,c) mp equiv =
 		  const_constraints = cst }
 	      in
 	      SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst
-      else
+      | _ ->
 	      (* Definition inside a sub-module *)
 	      let old = match spec with
 		| SFBmodule msb -> msb
@@ -156,7 +158,7 @@ and check_with_mod env sign (idl,mp1) mp equiv =
       let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in
       let before = List.rev rev_before in
       let env' = Modops.add_signature mp before equiv env in
-      if idl = [] then
+      match idl with [] ->
 	      (* Toplevel module definition *)
 	      let old = match spec with
 		  SFBmodule msb -> msb
@@ -191,7 +193,7 @@ and check_with_mod env sign (idl,mp1) mp equiv =
 	      let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in
 		SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
 	      add_delta_resolver equiv new_mb.mod_delta,cst
-      else
+      | _ ->
 	      (* Module definition of a sub-module *)
 	      let old = match spec with
 		  SFBmodule msb -> msb
diff --git a/kernel/names.ml b/kernel/names.ml
index 08b111cd6..c4e632a3a 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -96,10 +96,13 @@ let rec dir_path_ord (p1 : dir_path) (p2 : dir_path) =
     if Int.equal c 0 then dir_path_ord p1 p2 else c
   end
 
+let dir_path_eq p1 p2 = Int.equal (dir_path_ord p1 p2) 0
+
 let make_dirpath x = x
 let repr_dirpath x = x
 
 let empty_dirpath = []
+let is_empty_dirpath d = match d with [] -> true | _ -> false
 
 (** Printing of directory paths as ["coq_root.module.submodule"] *)
 
@@ -155,6 +158,7 @@ let string_of_label = string_of_id
 let pr_label l = str (string_of_label l)
 let id_of_label l = l
 let label_of_id id = id
+let eq_label = String.equal
 
 module Labset = Idset
 module Labmap = Idmap
@@ -281,7 +285,7 @@ let debug_string_of_con con =
 let debug_pr_con con = str (debug_string_of_con con)
 
 let con_with_label ((mp1,dp1,l1),(mp2,dp2,l2) as con) lbl =
-  if Int.equal (String.compare lbl l1) 0 && Int.equal (String.compare lbl l2) 0
+  if String.equal lbl l1 && String.equal lbl l2
     then con
     else ((mp1, dp1, lbl), (mp2, dp2, lbl))
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 5ab3b5c3f..3eb070380 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -45,6 +45,8 @@ type dir_path
 
 val dir_path_ord : dir_path -> dir_path -> int
 
+val dir_path_eq : dir_path -> dir_path -> bool
+
 (** Inner modules idents on top of list (to improve sharing).
    For instance: A.B.C is ["C";"B";"A"] *)
 val make_dirpath : module_ident list -> dir_path
@@ -52,6 +54,8 @@ val repr_dirpath : dir_path -> module_ident list
 
 val empty_dirpath : dir_path
 
+val is_empty_dirpath : dir_path -> bool
+
 (** Printing of directory paths as ["coq_root.module.submodule"] *)
 val string_of_dirpath : dir_path -> string
 
@@ -66,6 +70,8 @@ val pr_label : label -> Pp.std_ppcmds
 val label_of_id : identifier -> label
 val id_of_label : label -> identifier
 
+val eq_label : label -> label -> bool
+
 module Labset : Set.S with type elt = label
 module Labmap : Map.S with type key = label
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b0ea2f7db..fb6ffd2d1 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -333,14 +333,20 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 
     (* Eta-expansion on the fly *)
     | (FLambda _, _) ->
-        if v1 <> [] then
-	  anomaly "conversion was given unreduced term (FLambda)";
+        let () = match v1 with
+        | [] -> ()
+        | _ ->
+          anomaly "conversion was given unreduced term (FLambda)"
+        in
         let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
 	eqappr CONV l2r infos
 	  (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
     | (_, FLambda _) ->
-        if v2 <> [] then
-	  anomaly "conversion was given unreduced term (FLambda)";
+        let () = match v2 with
+        | [] -> ()
+        | _ ->
+	  anomaly "conversion was given unreduced term (FLambda)"
+	in
         let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
 	eqappr CONV l2r infos
 	  (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 143b22c34..28052c41b 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -271,7 +271,7 @@ let add_constant dir l decl senv =
     | ConstantEntry ce -> translate_constant senv.env kn ce
     | GlobalRecipe r ->
       let cb = translate_recipe senv.env kn r in
-      if dir = empty_dirpath then hcons_const_body cb else cb
+      if is_empty_dirpath dir then hcons_const_body cb else cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
@@ -284,16 +284,19 @@ let add_constant dir l decl senv =
 (* Insertion of inductive types. *)
 
 let add_mind dir l mie senv =
-  if mie.mind_entry_inds = [] then
-    anomaly "empty inductive types declaration";
+  let () = match mie.mind_entry_inds with
+  | [] ->
+    anomaly "empty inductive types declaration"
             (* this test is repeated by translate_mind *)
+  | _ -> ()
+  in
   let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in
-  if l <> label_of_id id then
+  if not (eq_label l (label_of_id id)) then
     anomaly ("the label of inductive packet and its first inductive"^
 	     " type do not match");
   let kn = make_mind senv.modinfo.modpath dir l in
   let mib = translate_mind senv.env kn mie in
-  let mib = if mib.mind_hyps <> [] then mib else hcons_mind mib in
+  let mib = match mib.mind_hyps with [] -> hcons_mind mib | _ -> mib in
   let senv' = add_field (l,SFBmind mib) (I kn) senv in
   kn, senv'
 
@@ -358,7 +361,7 @@ let end_module l restype senv =
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
       | STRUCT params -> params, (List.length params > 0)
   in
-  if l <> modinfo.label then error_incompatible_labels l modinfo.label;
+  if not (eq_label l modinfo.label) then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_non_empty_local_context None;
   let functorize_struct tb =
     List.fold_left
@@ -494,8 +497,11 @@ let end_module l restype senv =
 (* Adding parameters to modules or module types *)
 
 let add_module_parameter mbid mte inl senv =
-  if  senv.revstruct <> [] or senv.loads <> [] then
-    anomaly "Cannot add a module parameter to a non empty module";
+  let () = match senv.revstruct, senv.loads with
+  | [], _ :: _ | _ :: _, [] ->
+    anomaly "Cannot add a module parameter to a non empty module"
+  | _ -> ()
+  in
   let mtb = translate_module_type senv.env (MPbound mbid) inl mte in
   let senv = 
     full_add_module (module_body_of_type (MPbound mbid) mtb) senv
@@ -559,7 +565,7 @@ let end_modtype l senv =
       | LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end ()
       | SIG params -> params
   in
-  if l <> modinfo.label then error_incompatible_labels l modinfo.label;
+  if not (eq_label l modinfo.label) then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_non_empty_local_context None;
   let auto_tb =
      SEBstruct (List.rev senv.revstruct)
@@ -629,10 +635,9 @@ type compiled_library =
 (* We check that only initial state Require's were performed before
    [start_library] was called *)
 
-let is_empty senv =
-  senv.revstruct = [] &&
-  senv.modinfo.modpath = initial_path &&
-  senv.modinfo.variant = NONE
+let is_empty senv = match senv.revstruct, senv.modinfo.variant with
+  | [], NONE -> mp_eq senv.modinfo.modpath initial_path
+  | _ -> false
 
 let start_library dir senv =
   if not (is_empty senv) then
@@ -677,7 +682,7 @@ let export senv dir =
   begin
     match modinfo.variant with
       | LIBRARY dp ->
-	  if dir <> dp then
+	  if not (dir_path_eq dir dp) then
 	    anomaly "We are not exporting the right library!"
       | _ ->
 	  anomaly "We are not exporting the library"
@@ -703,7 +708,7 @@ let check_imports senv needed =
   let check (id,stamp) =
     try
       let actual_stamp = List.assoc id imports in
-      if stamp <> actual_stamp then
+      if not (String.equal stamp actual_stamp) then
 	error
 	  ("Inconsistent assumptions over module "^(string_of_dirpath id)^".")
     with Not_found ->
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 8b34950da..6aaf5b47d 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -135,14 +135,14 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   in
 
   let check_packet cst p1 p2 =
-    let check f why = if f p1 <> f p2 then error why in
-      check (fun p -> p.mind_consnames) NotSameConstructorNamesField;
-      check (fun p -> p.mind_typename) NotSameInductiveNameInBlockField;
+    let check f test why = if not (test (f p1) (f p2)) then error why in
+      check (fun p -> p.mind_consnames) (Array.equal id_eq) NotSameConstructorNamesField;
+      check (fun p -> p.mind_typename) id_eq NotSameInductiveNameInBlockField;
       (* nf_lc later *)
       (* nf_arity later *)
       (* user_lc ignored *)
       (* user_arity ignored *)
-      check (fun p -> p.mind_nrealargs) (NotConvertibleInductiveField p2.mind_typename); (* How can it fail since the type of inductive are checked below? [HH] *)
+      check (fun p -> p.mind_nrealargs) Int.equal (NotConvertibleInductiveField p2.mind_typename); (* How can it fail since the type of inductive are checked below? [HH] *)
       (* kelim ignored *)
       (* listrec ignored *)
       (* finite done *)
@@ -161,10 +161,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
       (arities_of_specif kn1 (mib1,p1))
       (arities_of_specif kn1 (mib2,p2))
   in
-  let check f why = if f mib1 <> f mib2 then error (why (f mib2)) in
-  check (fun mib -> mib.mind_finite) (fun x -> FiniteInductiveFieldExpected x);
-  check (fun mib -> mib.mind_ntypes) (fun x -> InductiveNumbersFieldExpected x);
-  assert (mib1.mind_hyps=[] && mib2.mind_hyps=[]);
+  let check f test why = if not (test (f mib1) (f mib2)) then error (why (f mib2)) in
+  check (fun mib -> mib.mind_finite) (==) (fun x -> FiniteInductiveFieldExpected x);
+  check (fun mib -> mib.mind_ntypes) Int.equal (fun x -> InductiveNumbersFieldExpected x);
+  assert (List.is_empty mib1.mind_hyps && List.is_empty mib2.mind_hyps);
   assert (Array.length mib1.mind_packets >= 1
 	    && Array.length mib2.mind_packets >= 1);
 
@@ -173,17 +173,17 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   (* at the time of checking the inductive arities in check_packet. *)
   (* Notice that we don't expect the local definitions to match: only *)
   (* the inductive types and constructors types have to be convertible *)
-  check (fun mib -> mib.mind_nparams) (fun x -> InductiveParamsNumberField x);
+  check (fun mib -> mib.mind_nparams) Int.equal (fun x -> InductiveParamsNumberField x);
 
   begin
   match mind_of_delta reso2 kn2  with
-      | kn2' when kn2=kn2' -> ()
+      | kn2' when eq_mind kn2 kn2' -> ()
       | kn2' -> 
 	  if not (eq_mind (mind_of_delta reso1 kn1) (subst_ind subst2 kn2')) then 
 	    error NotEqualInductiveAliases
   end;
   (* we check that records and their field names are preserved. *)
-  check (fun mib -> mib.mind_record) (fun x -> RecordFieldExpected x);
+  check (fun mib -> mib.mind_record) (==) (fun x -> RecordFieldExpected x);
   if mib1.mind_record then begin
     let rec names_prod_letin t = match kind_of_term t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
@@ -198,7 +198,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     check (fun mib ->
       let nparamdecls = List.length mib.mind_params_ctxt in
       let names = names_prod_letin (mib.mind_packets.(0).mind_user_lc.(0)) in
-      snd (List.chop nparamdecls names))
+      snd (List.chop nparamdecls names)) (List.equal name_eq)
       (fun x -> RecordProjectionsExpected x);
   end;
   (* we first check simple things *)
@@ -265,7 +265,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 
   match info1 with
     | Constant cb1 ->
-      assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
+      let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in
       let cb1 = subst_const_body subst1 cb1 in
       let cb2 = subst_const_body subst2 cb2 in
       (* Start by checking types*)
@@ -295,7 +295,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "instantiated by an inductive type. Hint: you can rename the " ^
        "inductive type and give a definition to map the old name to the new " ^
        "name."));
-      assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
+      let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
       if constant_has_body cb2 then error DefinitionFieldExpected;
       let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
@@ -306,7 +306,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
        "name."));
-      assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
+      let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
       if constant_has_body cb2 then error DefinitionFieldExpected;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
       let ty2 = Typeops.type_of_constant_type env cb2.const_type in
diff --git a/kernel/term.ml b/kernel/term.ml
index 94aa7d968..627919f09 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -672,7 +672,7 @@ let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
 let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
 
 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
+  id_eq i1 i2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
 
 let eq_rel_declaration (n1, c1, t1) (n2, c2, t2) =
   name_eq n1 n2 && Option.Misc.compare eq_constr c1 c2 && eq_constr t1 t2
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 294d99eea..8509edaf9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -126,9 +126,12 @@ let extract_level env p =
   let _,c = dest_prod_assum env p in
   match kind_of_term c with Sort (Type u) -> Some u | _ -> None
 
-let extract_context_levels env =
-  List.fold_left
-    (fun l (_,b,p) -> if b=None then extract_level env p::l else l) []
+let extract_context_levels env l =
+  let fold l (_, b, p) = match b with
+  | None -> extract_level env p :: l
+  | _ -> l
+  in
+  List.fold_left fold [] l
 
 let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
   let params, ccl = dest_prod_assum env t in
@@ -227,12 +230,14 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        if engagement env = Some ImpredicativeSet then
+        begin match engagement env with
+        | Some ImpredicativeSet ->
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        else
+        | _ ->
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (sup u1 type0_univ)
+        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (sup type0_univ u2)
     (* Product rule (Prop,Type_i,Type_i) *)
@@ -348,7 +353,7 @@ let judge_of_case env ci pj cj lfj =
 
 let type_fixpoint env lna lar vdefj =
   let lt = Array.length vdefj in
-  assert (Array.length lar = lt);
+  assert (Int.equal (Array.length lar) lt);
   try
     conv_leq_vecti env (Array.map j_type vdefj) (Array.map (fun ty -> lift lt ty) lar)
   with NotConvertibleVect i ->
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 18bee0fb4..12ec4e222 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -105,9 +105,12 @@ let pr_uni = function
   | Max ([],[u]) ->
       str "(" ++ pr_uni_level u ++ str ")+1"
   | Max (gel,gtl) ->
+      let opt_sep = match gel, gtl with
+      | [], _ | _, [] -> mt ()
+      | _ -> pr_comma ()
+      in
       str "max(" ++ hov 0
-       (prlist_with_sep pr_comma pr_uni_level gel ++
-	  (if gel <> [] & gtl <> [] then pr_comma () else mt ()) ++
+       (prlist_with_sep pr_comma pr_uni_level gel ++ opt_sep ++
 	prlist_with_sep pr_comma
 	  (fun x -> str "(" ++ pr_uni_level x ++ str ")+1") gtl) ++
       str ")"
@@ -177,7 +180,8 @@ let is_type0_univ = function
   | u -> false
 
 let is_univ_variable = function
-  | Atom a when a<>UniverseLevel.Set -> true
+  | Atom UniverseLevel.Set -> false
+  | Atom _ -> true
   | _ -> false
 
 (* When typing [Prop] and [Set], there is no constraint on the level,
@@ -538,10 +542,10 @@ module Constraint = Set.Make(
     type t = univ_constraint
     let compare (u,c,v) (u',c',v') =
       let i = constraint_type_ord c c' in
-      if i <> 0 then i
+      if not (Int.equal i 0) then i
       else
 	let i' = UniverseLevel.compare u u' in
-	if i' <> 0 then i'
+	if not (Int.equal i' 0) then i'
 	else UniverseLevel.compare v v'
   end)
 
@@ -830,7 +834,7 @@ let solve_constraints_system levels level_bounds =
   let nind = Array.length v in
   for i=0 to nind-1 do
     for j=0 to nind-1 do
-      if i<>j & is_direct_sort_constraint levels.(j) v.(i) then
+      if not (Int.equal i j) && is_direct_sort_constraint levels.(j) v.(i) then
 	v.(i) <- sup v.(i) level_bounds.(j)
     done;
     for j=0 to nind-1 do
@@ -854,7 +858,10 @@ let subst_large_constraints =
 
 let no_upper_constraints u cst =
   match u with
-  | Atom u -> Constraint.for_all (fun (u1,_,_) -> u1 <> u) cst
+  | Atom u ->
+    let test (u1, _, _) =
+      not (Int.equal (UniverseLevel.compare u1 u) 0) in
+    Constraint.for_all test cst
   | Max _ -> anomaly "no_upper_constraints"
 
 (* Is u mentionned in v (or equals to v) ? *)
@@ -871,10 +878,14 @@ let pr_arc = function
   | _, Canonical {univ=u; lt=[]; le=[]} ->
       mt ()
   | _, Canonical {univ=u; lt=lt; le=le} ->
+      let opt_sep = match lt, le with
+      | [], _ | _, [] -> mt ()
+      | _ -> spc ()
+      in
       pr_uni_level u ++ str " " ++
       v 0
         (pr_sequence (fun v -> str "< " ++ pr_uni_level v) lt ++
-	 (if lt <> [] & le <> [] then spc () else mt()) ++
+	 opt_sep ++
          pr_sequence (fun v -> str "<= " ++ pr_uni_level v) le) ++
       fnl ()
   | u, Equiv v ->