33 files changed, 233 insertions, 224 deletions

diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index fd9394025a..c4c96c9b55 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -281,7 +281,7 @@ let assoc_defined id env = match Environ.lookup_named id env with
 | LocalDef (_, c, _) -> c
 | _ -> raise Not_found
 
-let ref_value_cache ({i_cache = cache} as infos) tab ref =
+let ref_value_cache ({i_cache = cache;_} as infos) tab ref =
   try
     Some (KeyTable.find tab ref)
   with Not_found ->
@@ -289,7 +289,7 @@ let ref_value_cache ({i_cache = cache} as infos) tab ref =
     let body =
       match ref with
 	| RelKey n ->
-          let open Context.Rel.Declaration in
+          let open! Context.Rel.Declaration in
           let i = n - 1 in
           let (d, _) =
             try Range.get cache.i_rels i
@@ -837,7 +837,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
     let pars = mib.Declarations.mind_nparams in
     let right = fapp_stack (f, s') in
-    let (depth, args, s) = strip_update_shift_app m s in
+    let (depth, args, _s) = strip_update_shift_app m s in
     (** Try to drop the params, might fail on partially applied constructors. *)
     let argss = try_drop_parameters depth pars args in
     let hstack = Array.map (fun p ->
@@ -925,7 +925,7 @@ and knht info e t stk =
     | Fix _ -> knh info (mk_clos2 e t) stk
     | Cast(a,_,_) -> knht info e a stk
     | Rel n -> knh info (clos_rel e n) stk
-    | Proj (p,c) -> knh info (mk_clos2 e t) stk
+    | Proj (_p,_c) -> knh info (mk_clos2 e t) stk
     | (Lambda _|Prod _|Construct _|CoFix _|Ind _|
        LetIn _|Const _|Var _|Evar _|Meta _|Sort _) ->
         (mk_clos2 e t, stk)
@@ -952,7 +952,7 @@ let rec knr info tab m stk =
       (match ref_value_cache info tab (RelKey k) with
           Some v -> kni info tab v stk
         | None -> (set_norm m; (m,stk)))
-  | FConstruct((ind,c),u) ->
+  | FConstruct((_ind,c),_u) ->
      let use_match = red_set info.i_flags fMATCH in
      let use_fix = red_set info.i_flags fFIX in
      if use_match || use_fix then
@@ -1018,7 +1018,7 @@ let rec zip_term zfun m stk =
         zip_term zfun h s
     | Zshift(n)::s ->
         zip_term zfun (lift n m) s
-    | Zupdate(rf)::s ->
+    | Zupdate(_rf)::s ->
         zip_term zfun m s
 
 (* Computes the strong normal form of a term.
@@ -1038,7 +1038,7 @@ let rec kl info tab m =
 and norm_head info tab m =
   if is_val m then (incr prune; term_of_fconstr m) else
     match m.term with
-      | FLambda(n,tys,f,e) ->
+      | FLambda(_n,tys,f,e) ->
           let (e',rvtys) =
             List.fold_left (fun (e,ctxt) (na,ty) ->
               (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt))
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index ed3bd866a4..c63795b295 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -126,8 +126,8 @@ let compare e1 e2 = match e1, e2 with
 | FVrel r1, FVrel r2 -> Int.compare r1 r2
 | FVrel _, (FVuniv_var _ | FVevar _) -> -1
 | FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2
-| FVuniv_var i1, (FVnamed _ | FVrel _) -> 1
-| FVuniv_var i1, FVevar _ -> -1
+| FVuniv_var _i1, (FVnamed _ | FVrel _) -> 1
+| FVuniv_var _i1, FVevar _ -> -1
 | FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1
 | FVevar e1, FVevar e2 -> Evar.compare e1 e2
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 5362f9a814..73620ae578 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -413,7 +413,7 @@ let code_makeblock ~stack_size ~arity ~tag cont =
     Kpush :: nest_block tag arity cont
   end
 
-let compile_structured_constant cenv sc sz cont =
+let compile_structured_constant _cenv sc sz cont =
   set_max_stack_size sz;
   Kconst sc :: cont
 
@@ -534,7 +534,7 @@ let rec compile_lam env cenv lam sz cont =
       comp_app compile_structured_constant compile_get_univ cenv
         (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont
 
-  | Llet (id,def,body) ->
+  | Llet (_id,def,body) ->
       compile_lam env cenv def sz
         (Kpush ::
          compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont))
@@ -561,7 +561,7 @@ let rec compile_lam env cenv lam sz cont =
     | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont
     end
 
-  | Lfix ((rec_args, init), (decl, types, bodies)) ->
+  | Lfix ((rec_args, init), (_decl, types, bodies)) ->
       let ndef = Array.length types in
       let rfv = ref empty_fv in
       let lbl_types = Array.make ndef Label.no in
@@ -594,7 +594,7 @@ let rec compile_lam env cenv lam sz cont =
 	(Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
 
 
-  | Lcofix(init, (decl,types,bodies)) ->
+  | Lcofix(init, (_decl,types,bodies)) ->
       let ndef = Array.length types in
       let lbl_types = Array.make ndef Label.no in
       let lbl_bodies = Array.make ndef Label.no in
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 31dede6f5d..c21ce22421 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -107,7 +107,7 @@ let rec pp_lam lam =
   | Lval _ -> str "values"
   | Lsort s -> pp_sort s
   | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i
-  | Lprim((kn,_u),ar,op,args) ->
+  | Lprim((kn,_u),_ar,_op,args) ->
     hov 1
       (str "(PRIM " ++ pr_con kn ++  spc() ++
        prlist_with_sep spc pp_lam  (Array.to_list args) ++
@@ -215,7 +215,7 @@ let rec map_lam_with_binders g f n lam =
     let u' = map_uint g f n u in
     if u == u' then lam else Luint u'
 
-and map_uint g f n u =
+and map_uint _g f n u =
   match u with
   | UintVal _ -> u
   | UintDigits(args) ->
@@ -532,7 +532,7 @@ struct
     size = 0;
   }
 
-  let extend v =
+  let extend (v : 'a t) =
     if v.size = Array.length v.elems then
       let new_size = min (2*v.size) Sys.max_array_length in
       if new_size <= v.size then raise (Invalid_argument "Vect.extend");
@@ -545,12 +545,12 @@ struct
     v.elems.(v.size) <- a;
     v.size <- v.size + 1
 
-  let popn v n =
+  let popn (v : 'a t) n =
     v.size <- max 0 (v.size - n)
 
   let pop v = popn v 1
 
-  let get_last v n =
+  let get_last (v : 'a t) n =
     if v.size <= n then raise
         (Invalid_argument "Vect.get:index out of bounds");
     v.elems.(v.size - n - 1)
@@ -715,7 +715,7 @@ let rec lambda_of_constr env c =
 
 and lambda_of_app env f args =
   match Constr.kind f with
-  | Const (kn,u as c) ->
+  | Const (kn,_u as c) ->
     let kn = get_alias env.global_env kn in
     (* spiwack: checks if there is a specific way to compile the constant
                 if there is not, Not_found is raised, and the function
diff --git a/kernel/constr.ml b/kernel/constr.ml
index c73fe7fbde..b25f38d630 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -360,17 +360,17 @@ let destConst c = match kind c with
 
 (* Destructs an existential variable *)
 let destEvar c = match kind c with
-  | Evar (kn, a as r) -> r
+  | Evar (_kn, _a as r) -> r
   | _ -> raise DestKO
 
 (* Destructs a (co)inductive type named kn *)
 let destInd c = match kind c with
-  | Ind (kn, a as r) -> r
+  | Ind (_kn, _a as r) -> r
   | _ -> raise DestKO
 
 (* Destructs a constructor *)
 let destConstruct c = match kind c with
-  | Construct (kn, a as r) -> r
+  | Construct (_kn, _a as r) -> r
   | _ -> raise DestKO
 
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
@@ -421,12 +421,12 @@ let fold f acc c = match kind c with
   | Lambda (_,t,c) -> f (f acc t) c
   | LetIn (_,b,t,c) -> f (f (f acc b) t) c
   | App (c,l) -> Array.fold_left f (f acc c) l
-  | Proj (p,c) -> f acc c
+  | Proj (_p,c) -> f acc c
   | Evar (_,l) -> Array.fold_left f acc l
   | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
-  | Fix (_,(lna,tl,bl)) ->
+  | Fix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
-  | CoFix (_,(lna,tl,bl)) ->
+  | CoFix (_,(_lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
 
 (* [iter f c] iters [f] on the immediate subterms of [c]; it is
@@ -441,7 +441,7 @@ let iter f c = match kind c with
   | Lambda (_,t,c) -> f t; f c
   | LetIn (_,b,t,c) -> f b; f t; f c
   | App (c,l) -> f c; Array.iter f l
-  | Proj (p,c) -> f c
+  | Proj (_p,c) -> f c
   | Evar (_,l) -> Array.iter f l
   | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
   | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
@@ -463,7 +463,7 @@ let iter_with_binders g f n c = match kind c with
   | App (c,l) -> f n c; Array.Fun1.iter f n l
   | Evar (_,l) -> Array.Fun1.iter f n l
   | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl
-  | Proj (p,c) -> f n c
+  | Proj (_p,c) -> f n c
   | Fix (_,(_,tl,bl)) ->
       Array.Fun1.iter f n tl;
       Array.Fun1.iter f (iterate g (Array.length tl) n) bl
@@ -483,19 +483,19 @@ let fold_constr_with_binders g f n acc c =
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (na,t,c) -> f (g  n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g  n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g  n) (f n (f n acc b) t) c
+  | Prod (_na,t,c) -> f (g  n) (f n acc t) c
+  | Lambda (_na,t,c) -> f (g  n) (f n acc t) c
+  | LetIn (_na,b,t,c) -> f (g  n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
-  | Proj (p,c) -> f n acc c
+  | Proj (_p,c) -> f n acc c
   | Evar (_,l) -> Array.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in
+      let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in
+      let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
@@ -963,11 +963,11 @@ let constr_ord_int f t1 t2 =
     | LetIn _, _ -> -1 | _, LetIn _ -> 1
     | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2
     | App _, _ -> -1 | _, App _ -> 1
-    | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2
+    | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2
     | Const _, _ -> -1 | _, Const _ -> 1
-    | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2
+    | Ind (ind1, _u1), Ind (ind2, _u2) -> ind_ord ind1 ind2
     | Ind _, _ -> -1 | _, Ind _ -> 1
-    | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2
+    | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2
     | Construct _, _ -> -1 | _, Construct _ -> 1
     | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
         ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2
@@ -1226,9 +1226,9 @@ let rec hash t =
       combinesmall 11 (combine (constructor_hash c) (Instance.hash u))
     | Case (_ , p, c, bl) ->
       combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl))
-    | Fix (ln ,(_, tl, bl)) ->
+    | Fix (_ln ,(_, tl, bl)) ->
       combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
-    | CoFix(ln, (_, tl, bl)) ->
+    | CoFix(_ln, (_, tl, bl)) ->
        combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl))
     | Meta n -> combinesmall 15 n
     | Rel n -> combinesmall 16 n
diff --git a/kernel/context.ml b/kernel/context.ml
index 4a7204b75c..3d98381fbb 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -142,8 +142,8 @@ struct
     (** Reduce all terms in a given declaration to a single value. *)
     let fold_constr f decl acc =
       match decl with
-      | LocalAssum (n,ty) -> f ty acc
-      | LocalDef (n,v,ty) -> f ty (f v acc)
+      | LocalAssum (_n,ty) -> f ty acc
+      | LocalDef (_n,v,ty) -> f ty (f v acc)
 
     let to_tuple = function
       | LocalAssum (na, ty) -> na, None, ty
@@ -151,7 +151,7 @@ struct
 
     let drop_body = function
       | LocalAssum _ as d -> d
-      | LocalDef (na, v, ty) -> LocalAssum (na, ty)
+      | LocalDef (na, _v, ty) -> LocalAssum (na, ty)
 
   end
 
@@ -356,7 +356,7 @@ struct
 
     let drop_body = function
       | LocalAssum _ as d -> d
-      | LocalDef (id, v, ty) -> LocalAssum (id, ty)
+      | LocalDef (id, _v, ty) -> LocalAssum (id, ty)
 
     let of_rel_decl f = function
       | Rel.Declaration.LocalAssum (na,t) ->
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 7ef63c1860..c74f2ab318 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -42,7 +42,7 @@ let empty = {
   cst_trstate = Cpred.full;
 }
 
-let get_strategy { var_opacity; cst_opacity } f = function
+let get_strategy { var_opacity; cst_opacity; _ } f = function
   | VarKey id ->
       (try Id.Map.find id var_opacity
       with Not_found -> default)
@@ -51,7 +51,7 @@ let get_strategy { var_opacity; cst_opacity } f = function
       with Not_found -> default)
   | RelKey _ -> Expand
 
-let set_strategy ({ var_opacity; cst_opacity } as oracle) k l =
+let set_strategy ({ var_opacity; cst_opacity; _ } as oracle) k l =
   match k with
   | VarKey id ->
     let var_opacity =
@@ -75,13 +75,13 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l =
     { oracle with cst_opacity; cst_trstate; }
   | RelKey _ -> CErrors.user_err Pp.(str "set_strategy: RelKey")
 
-let fold_strategy f { var_opacity; cst_opacity; } accu =
+let fold_strategy f { var_opacity; cst_opacity; _ } accu =
   let fvar id lvl accu = f (VarKey id) lvl accu in
   let fcst cst lvl accu = f (ConstKey cst) lvl accu in
   let accu = Id.Map.fold fvar var_opacity accu in
   Cmap.fold fcst cst_opacity accu
 
-let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate)
+let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate)
 
 (* Unfold the first constant only if it is "more transparent" than the
    second one. In case of tie, use the recommended default. *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 657478a106..b361e36bbf 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -91,7 +91,7 @@ let update_case_info cache ci modlist =
   try
     let ind, n =
       match share cache (IndRef ci.ci_ind) modlist with
-      | (IndRef f,(u,l)) -> (f, Array.length l)
+      | (IndRef f,(_u,l)) -> (f, Array.length l)
       | _ -> assert false in
     { ci with ci_ind = ind; ci_npar = ci.ci_npar + n }
   with Not_found ->
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index bb9231d000..8bef6aec42 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -173,7 +173,7 @@ and slot_for_fv env fv =
       | Some (v, _) -> v
       end
   | FVevar evk -> val_of_evar evk
-  | FVuniv_var idu ->
+  | FVuniv_var _idu ->
     assert false
 
 and eval_to_patch env (buff,pl,fv) =
@@ -192,5 +192,5 @@ and val_of_constr env c =
   | Some v -> eval_to_patch env (to_memory v)
   | None -> assert false
 
-let set_transparent_const kn = () (* !?! *)
-let set_opaque_const kn = () (* !?! *)
+let set_transparent_const _kn = () (* !?! *)
+let set_opaque_const _kn = () (* !?! *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 51ec3defb3..d995786d97 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -181,7 +181,7 @@ let subst_regular_ind_arity sub s =
     if uar' == s.mind_user_arity then s 
     else { mind_user_arity = uar'; mind_sort = s.mind_sort }
 
-let subst_template_ind_arity sub s = s
+let subst_template_ind_arity _sub s = s
 
 (* FIXME records *)
 let subst_ind_arity =
@@ -240,14 +240,14 @@ let inductive_polymorphic_context mib =
 let inductive_is_polymorphic mib =
   match mib.mind_universes with
   | Monomorphic_ind _ -> false
-  | Polymorphic_ind ctx -> true
-  | Cumulative_ind cumi -> true
+  | Polymorphic_ind _ctx -> true
+  | Cumulative_ind _cumi -> true
 
 let inductive_is_cumulative mib =
   match mib.mind_universes with
   | Monomorphic_ind _ -> false
-  | Polymorphic_ind ctx -> false
-  | Cumulative_ind cumi -> true
+  | Polymorphic_ind _ctx -> false
+  | Cumulative_ind _cumi -> true
 
 let inductive_make_projection ind mib ~proj_arg =
   match mib.mind_record with
diff --git a/kernel/dune b/kernel/dune
index 011af9c28c..a503238907 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -13,3 +13,8 @@
 
 (documentation
  (package coq))
+
+; In dev profile, we check the kernel against a more strict set of
+; warnings.
+(env
+ (dev (flags :standard -w +a-4-44-50)))
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 3bfcaa7f52..dffcd70282 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -296,12 +296,12 @@ let eq_named_context_val c1 c2 =
 
 (* A local const is evaluable if it is defined  *)
 
-open Context.Named.Declaration
-
 let named_type id env =
+  let open Context.Named.Declaration in
   get_type (lookup_named id env)
 
 let named_body id env =
+  let open Context.Named.Declaration in
   get_value (lookup_named id env)
 
 let evaluable_named id env =
@@ -333,7 +333,7 @@ let fold_named_context f env ~init =
   let rec fold_right env =
     match match_named_context_val env.env_named_context with
     | None -> init
-    | Some (d, v, rem) ->
+    | Some (d, _v, rem) ->
 	let env =
 	  reset_with_named_context rem env in
 	f env d (fold_right env)
@@ -415,7 +415,7 @@ let constant_type env (kn,u) =
   let cb = lookup_constant kn env in
   match cb.const_universes with
   | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
-  | Polymorphic_const ctx -> 
+  | Polymorphic_const _ctx ->
     let csts = constraints_of cb u in
     (subst_instance_constr u cb.const_type, csts)
 
@@ -508,14 +508,14 @@ let get_projections env ind =
   Declareops.inductive_make_projections ind mib
 
 (* Mutual Inductives *)
-let polymorphic_ind (mind,i) env =
+let polymorphic_ind (mind,_i) env =
   Declareops.inductive_is_polymorphic (lookup_mind mind env)
 
 let polymorphic_pind (ind,u) env =
   if Univ.Instance.is_empty u then false
   else polymorphic_ind ind env
 
-let type_in_type_ind (mind,i) env =
+let type_in_type_ind (mind,_i) env =
   not (lookup_mind mind env).mind_typing_flags.check_universes
 
 let template_polymorphic_ind (mind,i) env =
@@ -527,7 +527,7 @@ let template_polymorphic_pind (ind,u) env =
   if not (Univ.Instance.is_empty u) then false
   else template_polymorphic_ind ind env
   
-let add_mind_key kn (mind, _ as mind_key) env =
+let add_mind_key kn (_mind, _ as mind_key) env =
   let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
   let new_globals =
     { env.env_globals with
@@ -543,7 +543,7 @@ let lookup_constant_variables c env =
   let cmap = lookup_constant c env in
   Context.Named.to_vars cmap.const_hyps
 
-let lookup_inductive_variables (kn,i) env =
+let lookup_inductive_variables (kn,_i) env =
   let mis = lookup_mind kn env in
   Context.Named.to_vars mis.mind_hyps
 
@@ -579,6 +579,7 @@ let global_vars_set env constr =
    contained in the types of the needed variables. *)
 
 let really_needed env needed =
+  let open! Context.Named.Declaration in
   Context.Named.fold_inside
     (fun need decl ->
       if Id.Set.mem (get_id decl) need then
@@ -594,6 +595,7 @@ let really_needed env needed =
     (named_context env)
 
 let keep_hyps env needed =
+  let open Context.Named.Declaration in
   let really_needed = really_needed env needed in
   Context.Named.fold_outside
     (fun d nsign ->
@@ -647,6 +649,7 @@ type unsafe_type_judgment = types punsafe_type_judgment
 exception Hyp_not_found
 
 let apply_to_hyp ctxt id f =
+  let open Context.Named.Declaration in
   let rec aux rtail ctxt =
     match match_named_context_val ctxt with
     | Some (d, v, ctxt) ->
@@ -663,6 +666,7 @@ let remove_hyps ids check_context check_value ctxt =
   let rec remove_hyps ctxt = match match_named_context_val ctxt with
   | None -> empty_named_context_val, false
   | Some (d, v, rctxt) ->
+     let open Context.Named.Declaration in
     let (ans, seen) = remove_hyps rctxt in
     if Id.Set.mem (get_id d) ids then (ans, true)
     else if not seen then ctxt, false
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 7abf8027bd..b976469ff7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -242,7 +242,7 @@ let check_subtyping cumi paramsctxt env_ar inds =
     in
     let env = Environ.add_constraints subtyp_constraints env in
     (* process individual inductive types: *)
-    Array.iter (fun (id,cn,lc,(sign,arity)) ->
+    Array.iter (fun (_id,_cn,lc,(_sign,arity)) ->
       match arity with
         | RegularArity (_, full_arity, _) ->
            check_subtyping_arity_constructor env dosubst full_arity numparams true;
@@ -368,7 +368,7 @@ let typecheck_inductive env mie =
 	  RegularArity (not is_natural,full_arity,defu)
       in
       let template_polymorphic () =
-        let _, s =
+        let _sign, s =
           try dest_arity env full_arity
           with NotArity -> raise (InductiveError (NotAnArity (env, full_arity)))
         in
@@ -428,7 +428,7 @@ exception IllFormedInd of ill_formed_ind
 let mind_extract_params = decompose_prod_n_assum
 
 let explain_ind_err id ntyp env nparamsctxt c err =
-  let (lparams,c') = mind_extract_params nparamsctxt c in
+  let (_lparams,c') = mind_extract_params nparamsctxt c in
   match err with
     | LocalNonPos kt ->
 	raise (InductiveError (NonPos (env,c',mkRel (kt+nparamsctxt))))
@@ -596,7 +596,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
                 discharged to the [check_positive_nested] function. *)
             if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec)
             else check_positive_nested ienv nmr (ind_kn, largs)
-	| err ->
+        | _err ->
             (** If an inductive of the mutually inductive block
                 appears in any other way, then the positivy check gives
                 up. *)
@@ -613,7 +613,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
       defined types, not one of the types of the mutually inductive
       block being defined). *)
   (* accesses to the environment are not factorised, but is it worth? *)
-  and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr ((mi,u), largs) =
+  and check_positive_nested (env,n,ntypes,_ra_env as ienv) nmr ((mi,u), largs) =
     let (mib,mip) = lookup_mind_specif env mi in
     let auxnrecpar = mib.mind_nparams_rec in
     let auxnnonrecpar = mib.mind_nparams - auxnrecpar in
@@ -664,7 +664,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
       the type [c]) is checked to be the right (properly applied)
       inductive type. *)
   and check_constructors ienv check_head nmr c =
-    let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c =
+    let rec check_constr_rec (env,n,ntypes,_ra_env as ienv) nmr lrec c =
       let x,largs = decompose_app (whd_all env c) in
 	match kind x with
 
@@ -813,7 +813,7 @@ let compute_projections (kn, i as ind) mib =
   in
   let projections decl (i, j, labs, pbs, letsubst) =
     match decl with
-    | LocalDef (na,c,t) ->
+    | LocalDef (_na,c,_t) ->
         (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
            to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
         let c = liftn 1 j c in
@@ -841,7 +841,7 @@ let compute_projections (kn, i as ind) mib =
         (i + 1, j + 1, lab :: labs, projty :: pbs, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
   in
-  let (_, _, labs, pbs, letsubst) =
+  let (_, _, labs, pbs, _letsubst) =
     List.fold_right projections ctx (0, 1, [], [], paramsletsubst)
   in
     Array.of_list (List.rev labs),
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 1d2f22b006..9bbcf07f7e 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -154,10 +154,10 @@ let make_subst env =
   let rec make subst = function
     | LocalDef _ :: sign, exp, args ->
         make subst (sign, exp, args)
-    | d::sign, None::exp, args ->
+    | _d::sign, None::exp, args ->
         let args = match args with _::args -> args | [] -> [] in
         make subst (sign, exp, args)
-    | d::sign, Some u::exp, a::args ->
+    | _d::sign, Some u::exp, a::args ->
         (* We recover the level of the argument, but we don't change the *)
         (* level in the corresponding type in the arity; this level in the *)
         (* arity is a global level which, at typing time, will be enforce *)
@@ -165,7 +165,7 @@ let make_subst env =
         (* a useless extra constraint *)
         let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in
           make (cons_subst u s subst) (sign, exp, args)
-    | LocalAssum (na,t) :: sign, Some u::exp, [] ->
+    | LocalAssum (_na,_t) :: sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
         (* template, it is identity substitution  otherwise (ie. when u is *)
@@ -173,7 +173,7 @@ let make_subst env =
         (* update its image [x] by [sup x u] in order not to forget the *)
         (* dependency in [u] that remains to be fullfilled. *)
         make (remember_subst u subst) (sign, exp, [])
-    | sign, [], _ ->
+    | _sign, [], _ ->
         (* Uniform parameters are exhausted *)
         subst
     | [], _, _ ->
@@ -199,7 +199,7 @@ let instantiate_universes env ctx ar argsorts =
 
 (* Type of an inductive type *)
 
-let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+let type_of_inductive_gen ?(polyprop=true) env ((_mib,mip),u) paramtyps =
   match mip.mind_arity with
   | RegularArity a -> subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
@@ -215,12 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
 let type_of_inductive env pind = 
   type_of_inductive_gen env pind [||]
 
-let constrained_type_of_inductive env ((mib,mip),u as pind) =
+let constrained_type_of_inductive env ((mib,_mip),u as pind) =
   let ty = type_of_inductive env pind in
   let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
-let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
+let constrained_type_of_inductive_knowing_parameters env ((mib,_mip),u as pind) args =
   let ty = type_of_inductive_gen env pind args in
   let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
@@ -249,7 +249,7 @@ let type_of_constructor (cstr, u) (mib,mip) =
   if i > nconstr then user_err Pp.(str "Not enough constructors in the type.");
   constructor_instantiate (fst ind) u mib specif.(i-1)
 
-let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) =
+let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) =
   let ty = type_of_constructor cstru ind in
   let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
@@ -279,7 +279,7 @@ let inductive_sort_family mip =
 let mind_arity mip =
   mip.mind_arity_ctxt, inductive_sort_family mip
 
-let get_instantiated_arity (ind,u) (mib,mip) params =
+let get_instantiated_arity (_ind,u) (mib,mip) params =
   let sign, s = mind_arity mip in
   full_inductive_instantiate mib u params sign, s
 
@@ -563,7 +563,7 @@ let check_inductive_codomain env p =
   let env = push_rel_context absctx env in
   let arctx, s = dest_prod_assum env ar in
   let env = push_rel_context arctx env in
-  let i,l' = decompose_app (whd_all env s) in
+  let i,_l' = decompose_app (whd_all env s) in
   isInd i
 
 (* The following functions are almost duplicated from indtypes.ml, except
@@ -635,10 +635,10 @@ let get_recargs_approx env tree ind args =
 			   build_recargs_nested ienv tree (ind_kn, largs)
 	     | _ -> mk_norec
        end
-    | err ->
+    | _err ->
        mk_norec
 
-  and build_recargs_nested (env,ra_env as ienv) tree (((mind,i),u), largs) =
+  and build_recargs_nested (env,_ra_env as ienv) tree (((mind,i),u), largs) =
     (* If the inferred tree already disallows recursion, no need to go further *)
     if eq_wf_paths tree mk_norec then tree
     else
@@ -676,7 +676,7 @@ let get_recargs_approx env tree ind args =
     (Rtree.mk_rec irecargs).(i)
 
   and build_recargs_constructors ienv trees c =
-    let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c =
+    let rec recargs_constr_rec (env,_ra_env as ienv) trees lrec c =
       let x,largs = decompose_app (whd_all env c) in
 	match kind x with
 
@@ -685,7 +685,7 @@ let get_recargs_approx env tree ind args =
              let recarg = build_recargs ienv (List.hd trees) b in
              let ienv' = ienv_push_var ienv (na,b,mk_norec) in
              recargs_constr_rec ienv' (List.tl trees) (recarg::lrec) d
-          | hd ->
+          | _hd ->
              List.rev lrec
     in
     recargs_constr_rec ienv trees [] c
@@ -794,7 +794,7 @@ let rec subterm_specif renv stack t =
     | Proj (p, c) -> 
       let subt = subterm_specif renv stack c in
       (match subt with
-       | Subterm (s, wf) ->
+       | Subterm (_s, wf) ->
          (* We take the subterm specs of the constructor of the record *)
          let wf_args = (dest_subterms wf).(0) in
          (* We extract the tree of the projected argument *)
@@ -964,7 +964,7 @@ let check_one_fix renv recpos trees def =
                    else check_rec_call renv' [] body)
                 bodies
 
-        | Const (kn,u as cu) ->
+        | Const (kn,_u as cu) ->
             if evaluable_constant kn renv.env then
               try List.iter (check_rec_call renv []) l
               with (FixGuardError _ ) ->
@@ -983,7 +983,7 @@ let check_one_fix renv recpos trees def =
             check_rec_call renv [] a;
             check_rec_call (push_var_renv renv (x,a)) [] b
 
-        | CoFix (i,(_,typarray,bodies as recdef)) ->
+        | CoFix (_i,(_,typarray,bodies as recdef)) ->
             List.iter (check_rec_call renv []) l;
 	    Array.iter (check_rec_call renv []) typarray;
 	    let renv' = push_fix_renv renv recdef in
@@ -992,13 +992,13 @@ let check_one_fix renv recpos trees def =
         | (Ind _ | Construct _) ->
             List.iter (check_rec_call renv []) l
 
-	| Proj (p, c) ->
+        | Proj (_p, c) ->
            List.iter (check_rec_call renv []) l;
            check_rec_call renv [] c
 
         | Var id ->
             begin
-              let open Context.Named.Declaration in
+              let open! Context.Named.Declaration in
               match lookup_named id renv.env with
               | LocalAssum _ ->
                   List.iter (check_rec_call renv []) l
@@ -1129,10 +1129,10 @@ let check_one_cofix env nbfix def deftype =
 	      raise (CoFixGuardError (env,UnguardedRecursiveCall t))
             else if not(List.for_all (noccur_with_meta n nbfix) args) then
 	      raise (CoFixGuardError (env,NestedRecursiveOccurrences))
-	| Construct ((_,i as cstr_kn),u)  ->
+        | Construct ((_,i as cstr_kn),_u)  ->
             let lra = vlra.(i-1) in
             let mI = inductive_of_constructor cstr_kn in
-	    let (mib,mip) = lookup_mind_specif env mI in
+            let (mib,_mip) = lookup_mind_specif env mI in
             let realargs = List.skipn mib.mind_nparams args in
             let rec process_args_of_constr = function
               | (t::lr), (rar::lrar) ->
@@ -1157,7 +1157,7 @@ let check_one_cofix env nbfix def deftype =
             else
 	      raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a))
 
-	| CoFix (j,(_,varit,vdefs as recdef)) ->
+        | CoFix (_j,(_,varit,vdefs as recdef)) ->
             if List.for_all (noccur_with_meta n nbfix) args
             then
 	      if Array.for_all (noccur_with_meta n nbfix) varit then
@@ -1203,7 +1203,7 @@ let check_one_cofix env nbfix def deftype =
 (* The  function which checks that the whole block of definitions
    satisfies the guarded condition *)
 
-let check_cofix env (bodynum,(names,types,bodies as recdef)) =
+let check_cofix env (_bodynum,(names,types,bodies as recdef)) =
   let flags = Environ.typing_flags env in
   if flags.check_guarded then
     let nbfix = Array.length bodies in
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f1d08ef6dd..bff3092655 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -319,12 +319,12 @@ let subst_con sub cst =
 let subst_con_kn sub con =
   subst_con sub (con,Univ.Instance.empty)
 
-let subst_pcon sub (con,u as pcon) = 
-  try let con', can = subst_con0 sub pcon in 
+let subst_pcon sub (_con,u as pcon) =
+  try let con', _can = subst_con0 sub pcon in
 	con',u
   with No_subst -> pcon
 
-let subst_pcon_term sub (con,u as pcon) = 
+let subst_pcon_term sub (_con,u as pcon) =
   try let con', can = subst_con0 sub pcon in 
 	(con',u), can
   with No_subst -> pcon, mkConstU pcon
@@ -441,7 +441,7 @@ let replace_mp_in_kn mpfrom mpto kn =
 let rec mp_in_mp mp mp1 =
   match mp1 with
     | _ when ModPath.equal mp1 mp -> true
-    | MPdot (mp2,l) -> mp_in_mp mp mp2
+    | MPdot (mp2,_l) -> mp_in_mp mp mp2
     | _ -> false
 
 let subset_prefixed_by mp resolver =
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 9435f46c6b..424d329e09 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -138,7 +138,7 @@ let rec functor_smart_map fty f0 funct = match funct with
     let a' = f0 a in if a==a' then funct else NoFunctor a'
 
 let rec functor_iter fty f0 = function
-  |MoreFunctor (mbid,ty,e) -> fty ty; functor_iter fty f0 e
+  |MoreFunctor (_mbid,ty,e) -> fty ty; functor_iter fty f0 e
   |NoFunctor a -> f0 a
 
 (** {6 Misc operations } *)
@@ -171,7 +171,7 @@ let implem_iter fs fa impl = match impl with
 
 (** {6 Substitutions of modular structures } *)
 
-let id_delta x y = x
+let id_delta x _y = x
 
 let subst_with_body sub = function
   |WithMod(id,mp) as orig ->
@@ -200,7 +200,7 @@ let rec subst_structure sub do_delta sign =
 
 and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body =
   fun is_mod sub subst_impl do_delta mb ->
-  let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in
+  let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty; _ } = mb in
   let mp' = subst_mp sub mp in
   let sub =
     if ModPath.equal mp mp' then sub
@@ -371,7 +371,7 @@ and strengthen_sig mp_from struc mp_to reso = match struc with
     let item' = l,SFBmodule mb' in
     let reso',rest' = strengthen_sig mp_from rest mp_to reso in
     add_delta_resolver reso' mb.mod_delta, item':: rest'
-  |(l,SFBmodtype mty as item) :: rest ->
+  |(_l,SFBmodtype _mty as item) :: rest ->
     let reso',rest' = strengthen_sig mp_from rest mp_to reso in
     reso',item::rest'
 
@@ -628,7 +628,7 @@ let join_structure except otab s =
   let rec join_module : 'a. 'a generic_module_body -> unit = fun mb ->
     Option.iter join_expression mb.mod_type_alg;
     join_signature mb.mod_type
-  and join_field (l,body) = match body with
+  and join_field (_l,body) = match body with
     |SFBconst sb -> join_constant_body except otab sb
     |SFBmind _ -> ()
     |SFBmodule m ->
diff --git a/kernel/names.ml b/kernel/names.ml
index 933cefe993..6d33f233e9 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -207,7 +207,7 @@ struct
 
   let repr mbid = mbid
 
-  let to_string (i, s, p) =
+  let to_string (_i, s, p) =
     DirPath.to_string p ^ "." ^ s
 
   let debug_to_string (i, s, p) =
@@ -328,7 +328,7 @@ module ModPath = struct
   let rec dp = function
   | MPfile sl -> sl
   | MPbound (_,_,dp) -> dp
-  | MPdot (mp,l) -> dp mp
+  | MPdot (mp,_l) -> dp mp
 
   module Self_Hashcons = struct
     type t = module_path
@@ -420,7 +420,7 @@ module KerName = struct
   let hash kn =
     let h = kn.refhash in
     if h < 0 then
-      let { modpath = mp; dirpath = dp; knlabel = lbl; } = kn in
+      let { modpath = mp; dirpath = dp; knlabel = lbl; _ } = kn in
       let h = combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl) in
       (* Ensure positivity on all platforms. *)
       let h = h land 0x3FFFFFFF in
@@ -623,8 +623,8 @@ let constr_modpath (ind,_) = ind_modpath ind
 
 let ith_mutual_inductive (mind, _) i = (mind, i)
 let ith_constructor_of_inductive ind i = (ind, i)
-let inductive_of_constructor (ind, i) = ind
-let index_of_constructor (ind, i) = i
+let inductive_of_constructor (ind, _i) = ind
+let index_of_constructor (_ind, i) = i
 
 let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2
 let eq_user_ind (m1, i1) (m2, i2) =
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index eed25a4ca4..74b075f4a5 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1007,7 +1007,7 @@ let compile_prim decl cond paux =
  *)
   let rec opt_prim_aux paux =
     match paux with
-    | PAprim(prefix, kn, op, args) ->
+    | PAprim(_prefix, _kn, op, args) ->
 	let args = Array.map opt_prim_aux args in
 	app_prim (Coq_primitive(op,None)) args
 (*
@@ -1071,7 +1071,7 @@ let ml_of_instance instance u =
   match t with
   | Lrel(id ,i) -> get_rel env id i
   | Lvar id -> get_var env id
-  | Lmeta(mv,ty) ->
+  | Lmeta(mv,_ty) ->
      let tyn = fresh_lname Anonymous in
      let i = push_symbol (SymbMeta mv) in
      MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|])
@@ -1184,7 +1184,7 @@ let ml_of_instance instance u =
       let lf,env_n = push_rels (empty_env env.env_univ ()) ids in
       let t_params = Array.make ndef [||] in
       let t_norm_f = Array.make ndef (Gnorm (l,-1)) in
-      let mk_let envi (id,def) t = MLlet (id,def,t) in
+      let mk_let _envi (id,def) t = MLlet (id,def,t) in
       let mk_lam_or_let (params,lets,env) (id,def) =
         let ln,env' = push_rel env id in
         match def with
@@ -1217,7 +1217,7 @@ let ml_of_instance instance u =
          (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f) in
       (* Compilation of fix *)
       let fv_args = fv_args env fvn fvr in      
-      let lf, env = push_rels env ids in
+      let lf, _env = push_rels env ids in
       let lf_args = Array.map (fun id -> MLlocal id) lf in
       let mk_norm = MLapp(MLglobal norm, fv_args) in
       let mkrec i lname = 
@@ -1272,9 +1272,9 @@ let ml_of_instance instance u =
       let mk_norm = MLapp(MLglobal norm, fv_args) in
       let lnorm = fresh_lname Anonymous in
       let ltype = fresh_lname Anonymous in
-      let lf, env = push_rels env ids in
+      let lf, _env = push_rels env ids in
       let lf_args = Array.map (fun id -> MLlocal id) lf in
-      let upd i lname cont =
+      let upd i _lname cont =
 	let paramsi = t_params.(i) in
 	let pargsi = Array.map (fun id -> MLlocal id) paramsi in
 	let uniti = fresh_lname Anonymous in
@@ -1305,7 +1305,7 @@ let ml_of_instance instance u =
 	(lname, paramsi, body) in
       MLletrec(Array.mapi mkrec lf, lf_args.(start)) *)
 
-  | Lmakeblock (prefix,(cn,u),_,args) ->
+  | Lmakeblock (prefix,(cn,_u),_,args) ->
      let args = Array.map (ml_of_lam env l) args in
      MLconstruct(prefix,cn,args)
   | Lconstruct (prefix, (cn,u)) ->
@@ -1561,7 +1561,7 @@ let rec list_of_mp acc = function
 let list_of_mp mp = list_of_mp [] mp
 
 let string_of_kn kn =
-  let (mp,dp,l) = KerName.repr kn in
+  let (mp,_dp,l) = KerName.repr kn in
   let mp = list_of_mp mp in
   String.concat "_" mp ^ "_" ^ string_of_label l
 
@@ -1987,7 +1987,7 @@ let compile_mind mb mind stack =
 	       (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
     in
     let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
-    let add_proj proj_arg acc pb =
+    let add_proj proj_arg acc _pb =
       let tbl = ob.mind_reloc_tbl in
       (* Building info *)
       let ci = { ci_ind = ind; ci_npar = nparams;
@@ -2053,9 +2053,9 @@ let compile_mind_deps env prefix ~interactive
 let compile_deps env sigma prefix ~interactive init t =
   let rec aux env lvl init t =
   match kind t with
-  | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
+  | Ind ((mind,_),_u) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
-    let c,u = get_alias env c in
+    let c,_u = get_alias env c in
     let cb,(nameref,_) = lookup_constant_key c env in
     let (_, (_, const_updates)) = init in
     if is_code_loaded ~interactive nameref
@@ -2074,11 +2074,11 @@ let compile_deps env sigma prefix ~interactive init t =
       let comp_stack = code@comp_stack in
       let const_updates = Cmap_env.add c (nameref, name) const_updates in
       comp_stack, (mind_updates, const_updates)
-  | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind
+  | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix ~interactive init mind
   | Proj (p,c) ->
     let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in
     aux env lvl init c
-  | Case (ci, p, c, ac) ->
+  | Case (ci, _p, _c, _ac) ->
       let mind = fst ci.ci_ind in
       let init = compile_mind_deps env prefix ~interactive init mind in
       fold_constr_with_binders succ (aux env) lvl init t
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index c75dde843e..054b6a2d17 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -25,9 +25,9 @@ let rec conv_val env pb lvl v1 v2 cu =
     | Vfun f1, Vfun f2 ->
 	let v = mk_rel_accu lvl in
 	conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
-    | Vfun f1, _ ->
+    | Vfun _f1, _ ->
 	conv_val env CONV lvl v1 (fun x -> v2 x) cu
-    | _, Vfun f2 ->
+    | _, Vfun _f2 ->
 	conv_val env CONV lvl (fun x -> v1 x) v2 cu
     | Vaccu k1, Vaccu k2 ->
 	conv_accu env pb lvl k1 k2 cu
@@ -110,7 +110,7 @@ and conv_atom env pb lvl a1 a2 cu =
 	else
 	  if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
 	  else conv_fix env lvl t1 f1 t2 f2 cu 
-    | Aprod(_,d1,c1), Aprod(_,d2,c2) ->
+    | Aprod(_,d1,_c1), Aprod(_,d2,_c2) ->
        let cu = conv_val env CONV lvl d1 d2 cu in
        let v = mk_rel_accu lvl in
        conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index ab40c643f9..70cb8691c6 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -142,7 +142,7 @@ let rec map_lam_with_binders g f n lam =
     let args' = Array.Smart.map (f n) args in
     if args == args' then lam else Levar (evk, args')
 
-and map_uint g f n u =
+and map_uint _g f n u =
   match u with
   | UintVal _ -> u
   | UintDigits(prefix,c,args) ->
@@ -203,7 +203,7 @@ let can_subst lam =
 
 let can_merge_if bt bf =
   match bt, bf with
-  | Llam(idst,_), Llam(idsf,_) -> true
+  | Llam(_idst,_), Llam(_idsf,_) -> true
   | _ -> false
 
 let merge_if t bt bf =
@@ -370,7 +370,7 @@ module Cache =
 
 let is_lazy env prefix t =
   match kind t with
-  | App (f,args) ->
+  | App (f,_args) ->
      begin match kind f with
      | Construct (c,_) ->
        let gr = GlobRef.IndRef (fst c) in
@@ -431,7 +431,7 @@ let rec lambda_of_constr cache env sigma c =
 
   | Sort s -> Lsort s
 
-  | Ind (ind,u as pind) ->
+  | Ind (ind,_u as pind) ->
       let prefix = get_mind_prefix env (fst ind) in
       Lind (prefix, pind)
 
@@ -529,7 +529,7 @@ let rec lambda_of_constr cache env sigma c =
 
 and lambda_of_app cache env sigma f args =
   match kind f with
-  | Const (kn,u as c) ->
+  | Const (_kn,_u as c) ->
       let kn,u = get_alias env c in
       let cb = lookup_constant kn env in
       (try
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index f784509b6f..b4126dd68c 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -40,7 +40,7 @@ let include_dirs () =
   [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"]
 
 (* Pointer to the function linking an ML object into coq's toplevel *)
-let load_obj = ref (fun x -> () : string -> unit)
+let load_obj = ref (fun _x -> () : string -> unit)
 
 let rt1 = ref (dummy_value ())
 let rt2 = ref (dummy_value ())
@@ -113,7 +113,7 @@ let call_compiler ?profile:(profile=false) ml_filename =
     let res = CUnix.sys_command (ocamlfind ()) args in
     let res = match res with
       | Unix.WEXITED 0 -> true
-      | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+      | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
         warn_native_compiler_failed (Inl res); false
     in
     res, link_filename
@@ -158,7 +158,7 @@ let call_linker ?(fatal=true) prefix f upds =
   (try
     if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
     register_native_file prefix
-   with Dynlink.Error e as exn ->
+   with Dynlink.Error _ as exn ->
      let exn = CErrors.push exn in
      if fatal then iraise exn
      else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn));
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index f8b71e4564..303cb06c55 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -87,21 +87,21 @@ let discharge_direct_opaque ~cook_constr ci = function
   | Direct (d,cu) ->
       Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
 
-let join_opaque { opaque_val = prfs; opaque_dir = odp } = function
+let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> ignore(Future.join cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp then
         let fp = snd (Int.Map.find i prfs) in
         ignore(Future.join fp)
 
-let uuid_opaque { opaque_val = prfs; opaque_dir = odp } = function
+let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> Some (Future.uuid cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then Some (Future.uuid (snd (Int.Map.find i prfs)))
       else None
 
-let force_proof { opaque_val = prfs; opaque_dir = odp } = function
+let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) ->
       fst(Future.force cu)
   | Indirect (l,dp,i) ->
@@ -112,7 +112,7 @@ let force_proof { opaque_val = prfs; opaque_dir = odp } = function
       let c = Future.force pt in
       force_constr (List.fold_right subst_substituted l (from_val c))
 
-let force_constraints { opaque_val = prfs; opaque_dir = odp } = function
+let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> snd(Future.force cu)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
@@ -121,14 +121,14 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp } = function
         | None -> Univ.ContextSet.empty
         | Some u -> Future.force u
 
-let get_constraints { opaque_val = prfs; opaque_dir = odp } = function
+let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> Some(Future.chain cu snd)
   | Indirect (_,dp,i) ->
       if DirPath.equal dp odp
       then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
       else !get_univ dp i
 
-let get_proof { opaque_val = prfs; opaque_dir = odp } = function
+let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
   | Direct (_,cu) -> Future.chain cu fst
   | Indirect (l,dp,i) ->
       let pt =
@@ -144,7 +144,7 @@ let a_constr = Future.from_val (mkRel 1)
 let a_univ = Future.from_val Univ.ContextSet.empty
 let a_discharge : cooking_info list = []
 
-let dump { opaque_val = otab; opaque_len = n } =
+let dump { opaque_val = otab; opaque_len = n; _ } =
   let opaque_table = Array.make n a_constr in
   let univ_table = Array.make n a_univ in
   let disch_table = Array.make n a_discharge in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c701b53fe4..2abb4b485c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -53,9 +53,9 @@ let compare_stack_shape stk1 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
-    | (Zproj p1::s1, Zproj p2::s2) ->
+    | (Zproj _p1::s1, Zproj _p2::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
-    | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) ->
+    | (ZcaseT(_c1,_,_,_)::s1, ZcaseT(_c2,_,_,_)::s2) ->
         Int.equal bal 0 (* && c1.ci_ind  = c2.ci_ind *) && compare_rec 0 s1 s2
     | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) ->
         Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2
@@ -261,7 +261,7 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u
     s
   | Declarations.Polymorphic_ind _ ->
     cmp_instances u1 u2 s
-  | Declarations.Cumulative_ind cumi ->
+  | Declarations.Cumulative_ind _cumi ->
     let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in
     if not (Int.equal num_cnstr_args nargs) then
       cmp_instances u1 u2 s
@@ -296,7 +296,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
           (match (z1,z2) with
             | (Zlapp a1,Zlapp a2) -> 
 	       Array.fold_right2 f a1 a2 cu1
-	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
+            | (Zlproj (c1,_l1),Zlproj (c2,_l2)) ->
               if not (Projection.Repr.equal c1 c2) then
 		raise NotConvertible
 	      else cu1
@@ -498,7 +498,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
             eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv
 	| None -> 
 	   match c2 with
-	   | FConstruct ((ind2,j2),u2) ->
+           | FConstruct ((ind2,_j2),_u2) ->
 	      (try
 	      let v2, v1 =
                 eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
@@ -515,7 +515,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv
         | None -> 
 	   match c1 with
-	   | FConstruct ((ind1,j1),u1) ->
+           | FConstruct ((ind1,_j1),_u1) ->
  	      (try let v1, v2 =
                     eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
                    in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -554,14 +554,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
       else raise NotConvertible
 	  
     (* Eta expansion of records *)
-    | (FConstruct ((ind1,j1),u1), _) ->
+    | (FConstruct ((ind1,_j1),_u1), _) ->
       (try
     	 let v1, v2 =
             eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2)
          in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
-    | (_, FConstruct ((ind2,j2),u2)) ->
+    | (_, FConstruct ((ind2,_j2),_u2)) ->
       (try
     	 let v2, v1 =
             eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1)
@@ -659,14 +659,14 @@ let check_sort_cmp_universes env pb s0 s1 univs =
     | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible
     | Set, Prop -> raise NotConvertible
     | Set, Type u -> check_pb Univ.type0_univ u
-    | Type u, Prop -> raise NotConvertible
+    | Type _u, Prop -> raise NotConvertible
     | Type u, Set -> check_pb u Univ.type0_univ
     | Type u0, Type u1 -> check_pb u0 u1
 
 let checked_sort_cmp_universes env pb s0 s1 univs =
   check_sort_cmp_universes env pb s0 s1 univs; univs
 
-let check_convert_instances ~flex u u' univs =
+let check_convert_instances ~flex:_ u u' univs =
   if UGraph.check_eq_instances univs u u' then univs
   else raise NotConvertible
 
@@ -707,7 +707,7 @@ let infer_cmp_universes env pb s0 s1 univs =
     | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs
     | Set, Prop -> raise NotConvertible
     | Set, Type u -> infer_pb Univ.type0_univ u
-    | Type u, Prop -> raise NotConvertible
+    | Type _u, Prop -> raise NotConvertible
     | Type u, Set -> infer_pb u Univ.type0_univ
     | Type u0, Type u1 -> infer_pb u0 u1
 
@@ -781,7 +781,7 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
     env univs t1 t2 = 
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
-let default_conv cv_pb ?(l2r=false) env t1 t2 =
+let default_conv cv_pb ?l2r:_ env t1 t2 =
     gen_conv cv_pb env t1 t2
 
 let default_conv_leq = default_conv CUMUL
@@ -912,7 +912,7 @@ let is_arity env c =
   with NotArity -> false
 
 let eta_expand env t ty =
-  let ctxt, codom = dest_prod env ty in
+  let ctxt, _codom = dest_prod env ty in
   let ctxt',t = dest_lam env t in
   let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in
   let eta_args = List.rev_map mkRel (List.interval 1 d) in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 74042f9e04..bfe68671a2 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -138,7 +138,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
   let mib2 =  Declareops.subst_mind_body subst2 mib2 in
   let check_inductive_type cst name t1 t2 =
     check_conv (NotConvertibleInductiveField name)
-      cst (inductive_is_polymorphic mib1) infer_conv_leq env t1 t2
+      cst (inductive_is_polymorphic mib1) (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2
   in
 
   let check_packet cst p1 p2 =
@@ -162,10 +162,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
 	cst
   in
   let mind = MutInd.make1 kn1 in
-  let check_cons_types i cst p1 p2 =
+  let check_cons_types _i cst p1 p2 =
     Array.fold_left3
       (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst
-	(inductive_is_polymorphic mib1) infer_conv env t1 t2)
+        (inductive_is_polymorphic mib1) (infer_conv ?l2r:None ?evars:None ?ts:None) env t1 t2)
       cst
       p2.mind_consnames
       (arities_of_specif (mind, inst) (mib1, p1))
@@ -229,7 +229,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
   let check_conv cst poly f = check_conv_error error cst poly f in
   let check_type poly cst env t1 t2 =
     let err = NotConvertibleTypeField (env, t1, t2) in
-    check_conv err cst poly infer_conv_leq env t1 t2
+    check_conv err cst poly (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2
   in
   match info1 with
     | Constant cb1 ->
@@ -268,14 +268,14 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
 		 Anyway [check_conv] will handle that afterwards. *)
 	      let c1 = Mod_subst.force_constr lc1 in
 	      let c2 = Mod_subst.force_constr lc2 in
-	      check_conv NotConvertibleBodyField cst poly infer_conv env c1 c2))
-   | IndType ((kn,i),mind1) ->
+              check_conv NotConvertibleBodyField cst poly (infer_conv ?l2r:None ?evars:None ?ts:None) env c1 c2))
+   | IndType ((_kn,_i),_mind1) ->
        CErrors.user_err Pp.(str @@
        "The kernel does not recognize yet that a parameter can be " ^
        "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.")
-   | IndConstr (((kn,i),j),mind1) ->
+   | IndConstr (((_kn,_i),_j),_mind1) ->
       CErrors.user_err Pp.(str @@
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
diff --git a/kernel/term.ml b/kernel/term.ml
index 4851a9c0d0..795cdeb040 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -54,13 +54,13 @@ let mkProd_wo_LetIn decl c =
   let open Context.Rel.Declaration in
   match decl with
   | LocalAssum (na,t) -> mkProd (na, t, c)
-  | LocalDef (na,b,t) -> subst1 b c
+  | LocalDef (_na,b,_t) -> subst1 b c
 
 let mkNamedProd_wo_LetIn decl c =
   let open Context.Named.Declaration in
   match decl with
     | LocalAssum (id,t) -> mkNamedProd id t c
-    | LocalDef (id,b,t) -> subst1 b (subst_var id c)
+    | LocalDef (id,b,_t) -> subst1 b (subst_var id c)
 
 (* non-dependent product t1 -> t2 *)
 let mkArrow t1 t2 = mkProd (Anonymous, t1, t2)
@@ -81,7 +81,7 @@ let mkNamedLambda_or_LetIn decl c =
 (* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *)
 let prodn n env b =
   let rec prodrec = function
-    | (0, env, b)        -> b
+    | (0, _env, b)        -> b
     | (n, ((v,t)::l), b) -> prodrec (n-1,  l, mkProd (v,t,b))
     | _ -> assert false
   in
@@ -93,7 +93,7 @@ let compose_prod l b = prodn (List.length l) l b
 (* lamn n [xn:Tn;..;x1:T1;Gamma] b = [x1:T1]..[xn:Tn]b *)
 let lamn n env b =
   let rec lamrec = function
-    | (0, env, b)        -> b
+    | (0, _env, b)        -> b
     | (n, ((v,t)::l), b) -> lamrec (n-1,  l, mkLambda (v,t,b))
     | _ -> assert false
   in
@@ -276,7 +276,7 @@ let decompose_prod_n_assum n =
       | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> prodec_rec l n c
-      | c -> user_err (str  "decompose_prod_n_assum: not enough assumptions")
+      | _ -> user_err (str  "decompose_prod_n_assum: not enough assumptions")
   in
   prodec_rec Context.Rel.empty n
 
@@ -297,7 +297,7 @@ let decompose_lam_n_assum n =
       | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c
       | Cast (c,_,_)      -> lamdec_rec l n c
-      | c -> user_err (str "decompose_lam_n_assum: not enough abstractions")
+      | _c -> user_err (str "decompose_lam_n_assum: not enough abstractions")
   in
   lamdec_rec Context.Rel.empty n
 
@@ -313,7 +313,7 @@ let decompose_lam_n_decls n =
       | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
       | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> lamdec_rec l n c
-      | c -> user_err (str "decompose_lam_n_decls: not enough abstractions")
+      | _ -> user_err (str "decompose_lam_n_decls: not enough abstractions")
   in
   lamdec_rec Context.Rel.empty n
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f59e07098b..f39dde772a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -73,7 +73,7 @@ type _ trust =
 let uniq_seff_rev = SideEffects.repr
 let uniq_seff l =
   let ans = List.rev (SideEffects.repr l) in
-  List.map_append (fun { eff } -> eff) ans
+  List.map_append (fun { eff ; _ } -> eff) ans
 
 let empty_seff = SideEffects.empty
 let add_seff mb eff effs =
@@ -122,7 +122,7 @@ let inline_side_effects env body ctx side_eff =
         let subst = Cmap_env.add c (Inr var) subst in
         let ctx = Univ.ContextSet.union ctx univs in
         (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
-      | Polymorphic_const auctx ->
+      | Polymorphic_const _auctx ->
         (** Inline the term to emulate universe polymorphism *)
         let subst = Cmap_env.add c (Inl b) subst in
         (subst, var, ctx, args)
@@ -250,9 +250,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
       delay even in the polymorphic case.  *)
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
-		       const_entry_universes = Monomorphic_const_entry univs } as c) ->
+                       const_entry_universes = Monomorphic_const_entry univs; _ } as c) ->
       let env = push_context_set ~strict:true univs env in
-      let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
+      let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in
       let tyj = infer_type env typ in
       let proofterm =
         Future.chain body (fun ((body,uctx),side_eff) ->
@@ -288,8 +288,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
 
   (** Other definitions have to be processed immediately. *)
   | DefinitionEntry c ->
-      let { const_entry_type = typ; const_entry_opaque = opaque } = c in
-      let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
+      let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in
+      let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
       let (body, ctx), side_eff = Future.join body in
       let body, ctx, _ = match trust with
       | Pure -> body, ctx, []
@@ -348,7 +348,7 @@ let record_aux env s_ty s_bo =
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" v
 
-let build_constant_declaration kn env result =
+let build_constant_declaration _kn env result =
   let open Cooking in
   let typ = result.cook_type in
   let check declared inferred =
@@ -478,7 +478,7 @@ let export_eff eff =
   (eff.seff_constant, eff.seff_body, eff.seff_role)
 
 let export_side_effects mb env c =
-      let { const_entry_body = body } = c in
+      let { const_entry_body = body; _ } = c in
       let _, eff = Future.force body in
       let ce = { c with
         const_entry_body = Future.chain body
@@ -493,7 +493,7 @@ let export_side_effects mb env c =
       let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in
       let trusted = check_signatures mb signatures in
       let push_seff env eff =
-        let { seff_constant = kn; seff_body = cb } = eff in
+        let { seff_constant = kn; seff_body = cb ; _ } = eff in
         let env = Environ.add_constant kn cb env in
         match cb.const_universes with
         | Polymorphic_const _ -> env
@@ -511,7 +511,7 @@ let export_side_effects mb env c =
           if Int.equal sl 0 then
            let env, cbs =
              List.fold_left (fun (env,cbs) eff ->
-              let { seff_constant = kn; seff_body = ocb; seff_env = u } = eff in
+              let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
                let ce = constant_entry_of_side_effect ocb u in
                let cb = translate_constant Pure env kn ce in
                let eff = { eff with
@@ -543,7 +543,7 @@ let translate_recipe env kn r =
   let hcons = DirPath.is_empty dir in
   build_constant_declaration kn env (Cooking.cook_constant ~hcons r)
 
-let translate_local_def env id centry =
+let translate_local_def env _id centry =
   let open Cooking in
   let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in
   let centry = {
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 25c1cbff3a..7456ecea56 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -118,14 +118,14 @@ let check_hyps_inclusion env f c sign =
 (* Type of constants *)
 
 
-let type_of_constant env (kn,u as cst) =
+let type_of_constant env (kn,_u as cst) =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
   let ty, cu = constant_type env cst in
   let () = check_constraints cu env in
     ty
 
-let type_of_constant_in env (kn,u as cst) =
+let type_of_constant_in env (kn,_u as cst) =
   let cb = lookup_constant kn env in
   let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in
   constant_type_in env cst
@@ -142,7 +142,7 @@ let type_of_constant_in env (kn,u as cst) =
   and no upper constraint exists on the sort $s$, we don't need to compute $s$
 *)
 
-let type_of_abstraction env name var ty =
+let type_of_abstraction _env name var ty =
   mkProd (name, var, ty)
 
 (* Type of an application. *)
@@ -204,7 +204,7 @@ let sort_of_product env domsort rangsort =
 
   where j.uj_type is convertible to a sort s2
 *)
-let type_of_product env name s1 s2 =
+let type_of_product env _name s1 s2 =
   let s = sort_of_product env s1 s2 in
     mkSort s
 
@@ -247,7 +247,7 @@ let check_cast env c ct k expected_type =
    dynamic constraints of the form u<=v are enforced *)
 
 let type_of_inductive_knowing_parameters env (ind,u as indu) args =
-  let (mib,mip) as spec = lookup_mind_specif env ind in
+  let (mib,_mip) as spec = lookup_mind_specif env ind in
   check_hyps_inclusion env mkIndU indu mib.mind_hyps;
   let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters 
     env (spec,u) args
@@ -264,7 +264,7 @@ let type_of_inductive env (ind,u as indu) =
 
 (* Constructors. *)
 
-let type_of_constructor env (c,u as cu) =
+let type_of_constructor env (c,_u as cu) =
   let () =
     let ((kn,_),_) = c in
     let mib = lookup_mind kn env in
@@ -285,7 +285,7 @@ let check_branch_types env (ind,u) c ct lft explft =
     | Invalid_argument _ ->
         error_number_branches env (make_judge c ct) (Array.length explft)
 
-let type_of_case env ci p pt c ct lf lft =
+let type_of_case env ci p pt c ct _lf lft =
   let (pind, _ as indspec) =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (make_judge c ct) in
@@ -399,7 +399,7 @@ let rec execute env cstr =
         let lft = execute_array env lf in
           type_of_case env ci p pt c ct lf lft
 
-    | Fix ((vn,i as vni),recdef) ->
+    | Fix ((_vn,i as vni),recdef) ->
       let (fix_ty,recdef') = execute_recdef env recdef i in
       let fix = (vni,recdef') in
         check_fix env fix; fix_ty
@@ -432,12 +432,12 @@ and execute_array env = Array.map (execute env)
 
 (* Derived functions *)
 
-let universe_levels_of_constr env c =
+let universe_levels_of_constr _env c =
   let rec aux s c =
     match kind c with
-    | Const (c, u) ->
+    | Const (_c, u) ->
        LSet.fold LSet.add (Instance.levels u) s
-    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
+    | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) ->
        LSet.fold LSet.add (Instance.levels u) s
     | Sort u when not (Sorts.is_small u) ->
       let u = Sorts.univ_of_sort u in
@@ -530,7 +530,7 @@ let judge_of_product env x varj outj =
   make_judge (mkProd (x, varj.utj_val, outj.utj_val))
              (mkSort (sort_of_product env varj.utj_type outj.utj_type))
 
-let judge_of_letin env name defj typj j =
+let judge_of_letin _env name defj typj j =
   make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val))
              (subst1 defj.uj_val j.uj_type)
 
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 95d71965df..9ff51fca55 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -194,7 +194,7 @@ let check_universes_invariants g =
   UMap.iter (fun l u ->
     match u with
     | Canonical u ->
-      UMap.iter (fun v strict ->
+      UMap.iter (fun v _strict ->
           incr n_edges;
           let v = repr g v in
           assert (topo_compare u v = -1);
@@ -435,7 +435,7 @@ let reorder g u v =
     | n0::q0 ->
       (* Computing new root. *)
       let root, rank_rest =
-        List.fold_left (fun ((best, rank_rest) as acc) n ->
+        List.fold_left (fun ((best, _rank_rest) as acc) n ->
           if n.rank >= best.rank then n, best.rank else acc)
           (n0, min_int) q0
       in
@@ -809,7 +809,7 @@ let normalize_universes g =
   in
   UMap.fold (fun _ u g ->
     match u with
-    | Equiv u -> g
+    | Equiv _u -> g
     | Canonical u ->
       let _, u, g = get_ltle g u in
       let _, _, g = get_gtge g u in
@@ -821,7 +821,7 @@ let constraints_of_universes g =
   let uf = UF.create () in
   let constraints_of u v acc =
     match v with
-    | Canonical {univ=u; ltle} ->
+    | Canonical {univ=u; ltle; _} ->
       UMap.fold (fun v strict acc->
         let typ = if strict then Lt else Le in
         Constraint.add (u,typ,v) acc) ltle acc
@@ -943,7 +943,7 @@ let check_eq_instances g t1 t2 =
 (** Pretty-printing *)
 
 let pr_arc prl = function
-  | _, Canonical {univ=u; ltle} ->
+  | _, Canonical {univ=u; ltle; _} ->
     if UMap.is_empty ltle then mt ()
     else
       prl u ++ str " " ++
@@ -963,7 +963,7 @@ let pr_universes prl g =
 
 let dump_universes output g =
   let dump_arc u = function
-    | Canonical {univ=u; ltle} ->
+    | Canonical {univ=u; ltle; _} ->
         let u_str = Level.to_string u in
         UMap.iter (fun v strict ->
           let typ = if strict then Lt else Le in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 311477daca..747a901f45 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -86,7 +86,7 @@ struct
     | Level (n,d) as x -> 
       let d' = Names.DirPath.hcons d in
         if d' == d then x else Level (n,d')
-    | Var n as x -> x
+    | Var _n as x -> x
 
   open Hashset.Combine
 
@@ -206,13 +206,13 @@ module LMap = struct
   include M
 
   let union l r = 
-    merge (fun k l r -> 
+    merge (fun _k l r ->
       match l, r with
       | Some _, _ -> l
       | _, _ -> r) l r
 
   let subst_union l r = 
-    merge (fun k l r -> 
+    merge (fun _k l r ->
       match l, r with
       | Some (Some _), _ -> l
       | Some None, None -> l
@@ -365,14 +365,14 @@ struct
       else f v ++ str"+" ++ int n
 
     let is_level = function
-      | (v, 0) -> true
+      | (_v, 0) -> true
       | _ -> false
 
     let level = function
       | (v,0) -> Some v
       | _ -> None
 	
-    let get_level (v,n) = v
+    let get_level (v,_n) = v
 
     let map f (v, n as x) = 
       let v' = f v in 
@@ -582,7 +582,7 @@ struct
 	prl u2 ++ fnl () )  c (str "")
 
   let universes_of c =
-    fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty
+    fold (fun (u1, _op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty
 end
 
 let universes_of_constraints = Constraint.universes_of
@@ -907,7 +907,7 @@ let subst_instance_constraints s csts =
 type universe_instance = Instance.t
 
 type 'a puniverses = 'a * Instance.t
-let out_punivs (x, y) = x
+let out_punivs (x, _y) = x
 let in_punivs x = (x, Instance.empty)
 let eq_puniverses f (x, u) (y, u') =
   f x y && Instance.equal u u'
@@ -932,8 +932,8 @@ struct
   let hcons (univs, cst) =
     (Instance.hcons univs, hcons_constraints cst)
 
-  let instance (univs, cst) = univs
-  let constraints (univs, cst) = cst
+  let instance (univs, _cst) = univs
+  let constraints (_univs, cst) = cst
 
   let union (univs, cst) (univs', cst') =
     Instance.append univs univs', Constraint.union cst cst'
@@ -952,7 +952,7 @@ struct
   include UContext
 
   let repr (inst, cst) =
-    (Array.mapi (fun i l -> Level.var i) inst, cst)
+    (Array.mapi (fun i _l -> Level.var i) inst, cst)
 
   let instantiate inst (u, cst) =
     assert (Array.length u = Array.length inst);
@@ -988,8 +988,8 @@ struct
   let hcons (univs, variance) = (* should variance be hconsed? *)
     (UContext.hcons univs, variance)
 
-  let univ_context (univs, subtypcst) = univs
-  let variance (univs, variance) = variance
+  let univ_context (univs, _subtypcst) = univs
+  let variance (_univs, variance) = variance
 
   (** This function takes a universe context representing constraints
      of an inductive and produces a CumulativityInfo.t with the
@@ -1066,8 +1066,8 @@ struct
     if is_empty ctx then mt() else
       h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 
-  let constraints (univs, cst) = cst
-  let levels (univs, cst) = univs
+  let constraints (_univs, cst) = cst
+  let levels (univs, _cst) = univs
 
   let size (univs,_) = LSet.cardinal univs
 end
@@ -1155,7 +1155,7 @@ let make_inverse_instance_subst i =
       LMap.empty arr
 
 let make_abstract_instance (ctx, _) = 
-  Array.mapi (fun i l -> Level.var i) ctx
+  Array.mapi (fun i _l -> Level.var i) ctx
 
 let abstract_universes ctx =
   let instance = UContext.instance ctx in
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 0f588a6302..9d5d79124b 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -66,7 +66,7 @@ let isMeta c = match Constr.kind c with
 let noccur_with_meta n m term =
   let rec occur_rec n c = match Constr.kind c with
     | Constr.Rel p -> if n<=p && p<n+m then raise LocalOccur
-    | Constr.App(f,cl) ->
+    | Constr.App(f,_cl) ->
         (match Constr.kind f with
            | Constr.Cast (c,_,_) when isMeta c -> ()
            | Constr.Meta _ -> ()
@@ -188,7 +188,7 @@ let adjust_rel_to_rel_context sign n =
     let open RelDecl in
     match sign with
     | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p)
-    | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p)
+    | LocalDef (_,_c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p)
     | [] -> (0,n)
   in snd (aux sign)
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index d19bea5199..5965853e1e 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -11,7 +11,7 @@ open Csymtable
 let compare_zipper z1 z2 =
   match z1, z2 with
   | Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2)
-  | Zfix(f1,args1), Zfix(f2,args2) ->  Int.equal (nargs args1) (nargs args2)
+  | Zfix(_f1,args1), Zfix(_f2,args2) ->  Int.equal (nargs args1) (nargs args2)
   | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true
   | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false
 
@@ -84,7 +84,7 @@ and conv_whd env pb k whd1 whd2 cu =
 and conv_atom env pb k a1 stk1 a2 stk2 cu =
 (*  Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *)
   match a1, a2 with
-  | Aind ((mi,i) as ind1) , Aind ind2 ->
+  | Aind ((mi,_i) as ind1) , Aind ind2 ->
     if eq_ind ind1 ind2 && compare_stack stk1 stk2 then
       if Environ.polymorphic_ind ind1 env then
         let mib = Environ.lookup_mind mi env in
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 9917e94a35..eaf64ba4af 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -187,5 +187,5 @@ let apply_whd k whd =
       interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0
   | Vatom_stk(a,stk) ->
       apply_stack (val_of_atom a) stk v
-  | Vuniv_level lvl -> assert false
+  | Vuniv_level _lvl -> assert false
 
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 8edd49f77f..217ef4b8e5 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -100,7 +100,7 @@ let eq_structured_constant c1 c2 = match c1, c2 with
 | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
 | Const_univ_level _ , _ -> false
 | Const_val v1, Const_val v2 -> eq_structured_values v1 v2
-| Const_val v1, _ -> false
+| Const_val _v1, _ -> false
 
 let hash_structured_constant c =
   let open Hashset.Combine in
@@ -245,7 +245,7 @@ type id_key =
 | RelKey of Int.t
 | EvarKey of Evar.t
 
-let eq_id_key k1 k2 = match k1, k2 with
+let eq_id_key (k1 : id_key) (k2 : id_key) = match k1, k2 with
 | ConstKey c1, ConstKey c2 -> Constant.equal c1 c2
 | VarKey id1, VarKey id2 -> Id.equal id1 id2
 | RelKey n1, RelKey n2 -> Int.equal n1 n2
@@ -304,9 +304,9 @@ let uni_lvl_val (v : values) : Univ.Level.t =
         | Vfun _ -> str "Vfun"
         | Vfix _ -> str "Vfix"
         | Vcofix _ -> str "Vcofix"
-        | Vconstr_const i -> str "Vconstr_const"
-        | Vconstr_block b -> str "Vconstr_block"
-        | Vatom_stk (a,stk) -> str "Vatom_stk"
+        | Vconstr_const _i -> str "Vconstr_const"
+        | Vconstr_block _b -> str "Vconstr_block"
+        | Vatom_stk (_a,_stk) -> str "Vatom_stk"
         | _ -> assert false
       in
       CErrors.anomaly
@@ -444,7 +444,7 @@ struct
   type t = id_key
   let equal = eq_id_key
   open Hashset.Combine
-  let hash = function
+  let hash : t -> tag = function
   | ConstKey c -> combinesmall 1 (Constant.hash c)
   | VarKey id -> combinesmall 2 (Id.hash id)
   | RelKey i -> combinesmall 3 (Int.hash i)
@@ -658,7 +658,7 @@ and pr_whd w =
   | Vfix _ -> str "Vfix"
   | Vcofix _ -> str "Vcofix"
   | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")"
-  | Vconstr_block b -> str "Vconstr_block"
+  | Vconstr_block _b -> str "Vconstr_block"
   | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")"
   | Vuniv_level _ -> assert false)
 and pr_stack stk =
@@ -668,6 +668,6 @@ and pr_stack stk =
 and pr_zipper z =
   Pp.(match z with
   | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")"
-  | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")"
-  | Zswitch s -> str "Zswitch(...)"
+  | Zfix (_f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")"
+  | Zswitch _s -> str "Zswitch(...)"
   | Zproj c -> str "Zproj(" ++ Projection.Repr.print c ++ str ")")