Merge PR #7746: Many small cleanups removing unused arguments and functions

4 files changed, 24 insertions, 24 deletions

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index bcb71fe55..8f11e01c3 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -221,7 +221,7 @@ let allowed_sorts issmall isunit s =
 
 
 
-let compute_elim_sorts env_ar params mib arity lc =
+let compute_elim_sorts env_ar params arity lc =
   let inst = extended_rel_list 0 params in
   let env_params = push_rel_context params env_ar in
   let lc = Array.map
@@ -239,7 +239,7 @@ let compute_elim_sorts env_ar params mib arity lc =
   allowed_sorts small unit s
 
 
-let typecheck_one_inductive env params mib mip =
+let typecheck_one_inductive env params mip =
   (* mind_typename and mind_consnames not checked *)
   (* mind_reloc_tbl, mind_nb_constant, mind_nb_args not checked (VM) *)
   (* mind_arity_ctxt, mind_arity, mind_nrealargs DONE (typecheck_arity) *)
@@ -256,7 +256,7 @@ let typecheck_one_inductive env params mib mip =
   Array.iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls;
   (* mind_kelim: checked by positivity criterion ? *)
   let sorts =
-    compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in
+    compute_elim_sorts env params mip.mind_arity mip.mind_nf_lc in
   let reject_sort s = not (List.mem_f family_equal s sorts) in
   if List.exists reject_sort mip.mind_kelim then
     failwith "elimination not allowed";
@@ -355,7 +355,7 @@ let lambda_implicit_lift n a =
 
 (* This removes global parameters of the inductive types in lc (for
    nested inductive types only ) *)
-let abstract_mind_lc env ntyps npars lc =
+let abstract_mind_lc ntyps npars lc =
   if npars = 0 then
     lc
   else
@@ -448,7 +448,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc
       let auxntyp = mib.mind_ntypes in
 	if 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
+        let auxlcvect = abstract_mind_lc auxntyp auxnpar mip.mind_nf_lc in
 	  (* Extends the environment with a variable corresponding to
 	     the inductive def *)
 	let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in
@@ -625,7 +625,7 @@ let check_inductive env kn mib =
   (*  - check arities *)
   let env_ar = typecheck_arity env0 params mib.mind_packets in
   (*  - check constructor types *)
-  Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
+  Array.iter (typecheck_one_inductive env_ar params) mib.mind_packets;
   (* check the inferred subtyping relation *)
   let () = 
     match mib.mind_universes with
diff --git a/checker/inductive.ml b/checker/inductive.ml
index b1edec556..d15380643 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -797,7 +797,7 @@ let rec subterm_specif renv stack t =
 
       | Lambda (x,a,b) ->
           assert (l=[]);
-	  let spec,stack' = extract_stack renv a stack in
+          let spec,stack' = extract_stack stack in
 	    subterm_specif (push_var renv (x,a,spec)) stack' b
 
       (* Metas and evars are considered OK *)
@@ -813,7 +813,7 @@ and stack_element_specif = function
   |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h
   |SArg x -> x
 
-and extract_stack renv a = function
+and extract_stack = function
   | [] -> Lazy.from_val Not_subterm , []
   | h::t -> stack_element_specif h, t
 
@@ -845,7 +845,7 @@ let error_illegal_rec_call renv fx (arg_renv,arg) =
 let error_partial_apply renv fx =
   raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx))
 
-let filter_stack_domain env ci p stack =
+let filter_stack_domain env p stack =
   let absctx, ar = dest_lam_assum env p in
   (* Optimization: if the predicate is not dependent, no restriction is needed
      and we avoid building the recargs tree. *)
@@ -925,7 +925,7 @@ let check_one_fix renv recpos trees def =
             let case_spec = branches_specif renv 
 	      (lazy_subterm_specif renv [] c_0) ci in
 	    let stack' = push_stack_closures renv l stack in
-        let stack' = filter_stack_domain renv.env ci p stack' in
+        let stack' = filter_stack_domain renv.env p stack' in
               Array.iteri (fun k br' -> 
 			     let stack_br = push_stack_args case_spec.(k) stack' in
 			     check_rec_call renv stack_br br') lrest
@@ -968,7 +968,7 @@ let check_one_fix renv recpos trees def =
         | Lambda (x,a,b) ->
 	    assert (l = []);
 	    check_rec_call renv [] a ;
-	    let spec, stack' = extract_stack renv a stack in
+            let spec, stack' = extract_stack stack in
 	    check_rec_call (push_var renv (x,a,spec)) stack' b
 
         | Prod (x,a,b) ->
diff --git a/checker/modops.ml b/checker/modops.ml
index c7ad0977a..b92d7bbf1 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -80,7 +80,7 @@ and add_module mb env =
 
 let add_module_type mp mtb env = add_module (module_body_of_type mp mtb) env
 
-let strengthen_const mp_from l cb resolver =
+let strengthen_const mp_from l cb =
   match cb.const_body with
     | Def _ -> cb
     | _ ->
@@ -104,34 +104,34 @@ and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a ge
   match mb.mod_type with
   | MoreFunctor _ -> mb
   | NoFunctor sign ->
-    let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta
+    let resolve_out,sign_out = strengthen_sig mp_from sign mp_to
     in
     { mb with
       mod_expr = mk_expr mp_to;
       mod_type = NoFunctor sign_out;
       mod_delta = resolve_out }
 
-and strengthen_sig mp_from sign mp_to resolver =
+and strengthen_sig mp_from sign mp_to =
   match sign with
     | [] -> empty_delta_resolver,[]
     | (l,SFBconst cb) :: rest ->
-	let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+        let item' = l,SFBconst (strengthen_const mp_from l cb) in
+        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
 	resolve_out,item'::rest'
     | (_,SFBmind _ as item):: rest ->
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
 	  resolve_out,item::rest'
     | (l,SFBmodule mb) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
 	let mp_to' = MPdot(mp_to,l) in
 	let mb_out = strengthen_mod mp_from' mp_to' mb in
 	let item' = l,SFBmodule (mb_out) in
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
 	resolve_out (*add_delta_resolver resolve_out mb.mod_delta*),
-	item':: rest'
-    | (l,SFBmodtype mty as item) :: rest ->
-	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
-	resolve_out,item::rest'
+        item':: rest'
+    | (_,SFBmodtype _ as item) :: rest ->
+        let resolve_out,rest' = strengthen_sig mp_from rest mp_to in
+        resolve_out,item::rest'
 
 let strengthen mtb mp =
   strengthen_body ignore mtb.mod_mp mp mtb
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 6d0d6f6c6..3f7f84470 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -217,7 +217,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets
   in ()
 
-let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
+let check_constant env l info1 cb2 spec2 subst1 subst2 =
   let error () = error_not_match l spec2 in
   let check_conv f = check_conv_error error f in
   let check_type env t1 t2 = check_conv conv_leq env t1 t2 in
@@ -281,7 +281,7 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 =
   let check_one_body  (l,spec2) =
       match spec2 with
 	| SFBconst cb2 ->
-	    check_constant  env mp1 l (get_obj mp1 map1 l)
+            check_constant env l (get_obj mp1 map1 l)
 	      cb2 spec2 subst1 subst2
 	| SFBmind mib2 ->
 	    check_inductive env mp1 l (get_obj mp1 map1 l)