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

7 files changed, 55 insertions, 70 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 31496513a..b2a528a1f 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -322,8 +322,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
   try
 
   let f = funs.(i) in
-  let env = Global.env () in    
-  let type_sort = Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd InType in
+  let type_sort = Evarutil.evd_comb1 Evd.fresh_sort_in_family evd InType in
   let new_sorts =
     match sorts with
       | None -> Array.make (Array.length funs) (type_sort)
@@ -344,7 +343,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       (*     let id_of_f = Label.to_id (con_label f) in *)
       let register_with_sort fam_sort =
         let evd' = Evd.from_env (Global.env ()) in
-        let evd',s = Evd.fresh_sort_in_family env evd' fam_sort in
+        let evd',s = Evd.fresh_sort_in_family evd' fam_sort in
         let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
         let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
         let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
@@ -354,7 +353,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
           Evd.const_univ_entry ~poly evd'
         in
         let ce = Declare.definition_entry ~univs value in
-	ignore(
+        ignore(
 	  Declare.declare_constant
 	    name
 	    (DefinitionEntry ce,
@@ -508,8 +507,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
   let i = ref (-1) in
   let sorts =
     List.rev_map (fun (_,x) ->
-		  Evarutil.evd_comb1 (Evd.fresh_sort_in_family env) evd x
-	     )
+                  Evarutil.evd_comb1 Evd.fresh_sort_in_family evd x
+             )
       fas
   in
   (* We create the first priciple by tactic *)
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 09179dad3..4357689ee 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -115,7 +115,7 @@ let string_of_genarg_arg (ArgumentType arg) =
   let keyword x = tag_keyword (str x)
   let primitive x = tag_primitive (str x)
 
-  let has_type (Val.Dyn (tag, x)) t = match Val.eq tag t with
+  let has_type (Val.Dyn (tag, _)) t = match Val.eq tag t with
   | None -> false
   | Some _ -> true
 
@@ -188,7 +188,7 @@ let string_of_genarg_arg (ArgumentType arg) =
     | AN v -> f v
     | ByNotation (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc)
 
-  let pr_located pr (loc,x) = pr x
+  let pr_located pr (_,x) = pr x
 
   let pr_evaluable_reference = function
     | EvalVarRef id -> pr_id id
@@ -240,7 +240,7 @@ let string_of_genarg_arg (ArgumentType arg) =
     in
     pr_sequence (fun x -> x) l
 
-  let pr_extend_gen pr_gen lev { mltac_name = s; mltac_index = i } l =
+  let pr_extend_gen pr_gen _ { mltac_name = s; mltac_index = i } l =
       let name =
         str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
         str "@" ++ int i
@@ -260,7 +260,7 @@ let string_of_genarg_arg (ArgumentType arg) =
   | Extend.Uentry tag ->
     let ArgT.Any tag = tag in
     ArgT.repr tag
-  | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl
+  | Extend.Uentryl (_, lvl) -> "tactic" ^ string_of_int lvl
 
   let pr_alias_key key =
     try
@@ -288,7 +288,7 @@ let string_of_genarg_arg (ArgumentType arg) =
       let p = pr_tacarg_using_rule pr_gen prods in
       if pp.pptac_level > lev then surround p else p
     with Not_found ->
-      let pr arg = str "_" in
+      let pr _ = str "_" in
       KerName.print key ++ spc() ++ pr_sequence pr l ++ str" (* Generic printer *)"
 
   let pr_farg prtac arg = prtac (1, Any) (TacArg (Loc.tag arg))
@@ -341,14 +341,14 @@ let string_of_genarg_arg (ArgumentType arg) =
       pr_any_arg pr symb arg
     | _ -> str "ltac:(" ++ prtac (1, Any) arg ++ str ")"
 
-  let pr_raw_extend_rec prc prlc prtac prpat =
+  let pr_raw_extend_rec prtac =
     pr_extend_gen (pr_farg prtac)
-  let pr_glob_extend_rec prc prlc prtac prpat =
+  let pr_glob_extend_rec prtac =
     pr_extend_gen (pr_farg prtac)
 
-  let pr_raw_alias prc prlc prtac prpat lev key args =
+  let pr_raw_alias prtac lev key args =
     pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args
-  let pr_glob_alias prc prlc prtac prpat lev key args =
+  let pr_glob_alias prtac lev key args =
     pr_alias_gen (pr_targ (fun l a -> prtac l (TacArg (Loc.tag a)))) lev key args
 
   (**********************************************************************)
@@ -743,7 +743,7 @@ let pr_goal_selector ~toplevel s =
       (* Main tactic printer *)
       and pr_atom1 a = tag_atom a (match a with
         (* Basic tactics *)
-        | TacIntroPattern (ev,[]) as t ->
+        | TacIntroPattern (_,[]) as t ->
           pr_atom0 t
         | TacIntroPattern (ev,(_::_ as p)) ->
            hov 1 (primitive (if ev then "eintros" else "intros") ++
@@ -1054,7 +1054,7 @@ let pr_goal_selector ~toplevel s =
               primitive "fresh" ++ pr_fresh_ids l, latom
             | TacArg(_,TacGeneric arg) ->
               pr.pr_generic arg, latom
-            | TacArg(_,TacCall(loc,(f,[]))) ->
+            | TacArg(_,TacCall(_,(f,[]))) ->
               pr.pr_reference f, latom
             | TacArg(_,TacCall(loc,(f,l))) ->
               pr_with_comments ?loc (hov 1 (
@@ -1112,8 +1112,8 @@ let pr_goal_selector ~toplevel s =
       pr_reference = pr_qualid;
       pr_name = pr_lident;
       pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg);
-      pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
-      pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+      pr_extend = pr_raw_extend_rec pr_raw_tactic_level;
+      pr_alias = pr_raw_alias pr_raw_tactic_level;
     } in
     make_pr_tac
       pr raw_printers
@@ -1142,12 +1142,8 @@ let pr_goal_selector ~toplevel s =
         pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
         pr_name = pr_lident;
         pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg);
-        pr_extend = pr_glob_extend_rec
-          (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
-          prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
-        pr_alias = pr_glob_alias
-          (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
-          prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
+        pr_extend = pr_glob_extend_rec prtac;
+        pr_alias = pr_glob_alias prtac;
       } in
       make_pr_tac
         pr glob_printers
@@ -1168,8 +1164,8 @@ let pr_goal_selector ~toplevel s =
         | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
-  let pr_atomic_tactic_level env sigma n t =
-    let prtac n (t:atomic_tactic_expr) =
+  let pr_atomic_tactic_level env sigma t =
+    let prtac (t:atomic_tactic_expr) =
       let pr = {
         pr_tactic = (fun _ _ -> str "<tactic>");
         pr_constr = (fun c -> pr_econstr_env env sigma c);
@@ -1188,18 +1184,15 @@ let pr_goal_selector ~toplevel s =
       in
       pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
     in
-    prtac n t
+    prtac t
 
   let pr_raw_generic = Pputils.pr_raw_generic
 
   let pr_glb_generic = Pputils.pr_glb_generic
 
-  let pr_raw_extend env = pr_raw_extend_rec
-    pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
+  let pr_raw_extend _ = pr_raw_extend_rec pr_raw_tactic_level
 
-  let pr_glob_extend env = pr_glob_extend_rec
-    (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
-    (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+  let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env)
 
   let pr_alias pr lev key args =
     pr_alias_gen (fun _ arg -> pr arg) lev key args
@@ -1207,14 +1200,14 @@ let pr_goal_selector ~toplevel s =
   let pr_extend pr lev ml args =
     pr_extend_gen pr lev ml args
 
-  let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma ltop c
+  let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma c
 
 let declare_extra_genarg_pprule wit
   (f : 'a raw_extra_genarg_printer)
   (g : 'b glob_extra_genarg_printer)
   (h : 'c extra_genarg_printer) =
   begin match wit with
-    | ExtraArg s -> ()
+    | ExtraArg _ -> ()
     | _          -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
   end;
   let f x =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 01c52c413..9f8cd2fc4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -409,7 +409,7 @@ module TypeGlobal = struct
 
 
   let inverse env (evd,cstrs) car rel = 
-    let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in
+    let (evd, sort) = Evarutil.new_Type ~rigid:Evd.univ_flexible evd in
       app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
 
 end
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 84baea964..026c00b84 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -165,8 +165,7 @@ let coerce_var_to_ident fresh env sigma v =
 (* Interprets, if possible, a constr to an identifier which may not
    be fresh but suitable to be given to the fresh tactic. Works for
    vars, constants, inductive, constructors and sorts. *)
-let coerce_to_ident_not_fresh env sigma v =
-let g = sigma in
+let coerce_to_ident_not_fresh sigma v =
 let id_of_name = function
   | Name.Anonymous -> Id.of_string "x"
   | Name.Name x -> x in
@@ -183,9 +182,9 @@ let id_of_name = function
     | Some c ->
        match EConstr.kind sigma c with
        | Var id -> id 
-       | Meta m -> id_of_name (Evd.meta_name g m)
+       | Meta m -> id_of_name (Evd.meta_name sigma m)
        | Evar (kn,_) ->
-        begin match Evd.evar_ident kn g with
+        begin match Evd.evar_ident kn sigma with
         | None -> fail ()
         | Some id -> id
         end
@@ -208,7 +207,7 @@ let id_of_name = function
        | _ -> fail()
 
 
-let coerce_to_intro_pattern env sigma v =
+let coerce_to_intro_pattern sigma v =
   if has_type v (topwit wit_intro_pattern) then
     (out_gen (topwit wit_intro_pattern) v).CAst.v
   else if has_type v (topwit wit_var) then
@@ -221,8 +220,8 @@ let coerce_to_intro_pattern env sigma v =
       IntroNaming (IntroIdentifier (destVar sigma c))
   | _ -> raise (CannotCoerceTo "an introduction pattern")
 
-let coerce_to_intro_pattern_naming env sigma v =
-  match coerce_to_intro_pattern env sigma v with
+let coerce_to_intro_pattern_naming sigma v =
+  match coerce_to_intro_pattern sigma v with
   | IntroNaming pat -> pat
   | _ -> raise (CannotCoerceTo "a naming introduction pattern")
 
@@ -255,7 +254,7 @@ let coerce_to_constr env v =
     (try [], constr_of_id env id with Not_found -> fail ())
   else fail ()
 
-let coerce_to_uconstr env v =
+let coerce_to_uconstr v =
   if has_type v (topwit wit_uconstr) then
     out_gen (topwit wit_uconstr) v
   else
@@ -299,11 +298,11 @@ let coerce_to_constr_list env v =
     List.map map l
   | None -> raise (CannotCoerceTo "a term list")
 
-let coerce_to_intro_pattern_list ?loc env sigma v =
+let coerce_to_intro_pattern_list ?loc sigma v =
   match Value.to_list v with
   | None -> raise (CannotCoerceTo "an intro pattern list")
   | Some l ->
-    let map v = CAst.make ?loc @@ coerce_to_intro_pattern env sigma v in
+    let map v = CAst.make ?loc @@ coerce_to_intro_pattern sigma v in
     List.map map l
 
 let coerce_to_hyp env sigma v =
@@ -328,7 +327,7 @@ let coerce_to_hyp_list env sigma v =
   | None -> raise (CannotCoerceTo "a variable list")
 
 (* Interprets a qualified name *)
-let coerce_to_reference env sigma v =
+let coerce_to_reference sigma v =
   match Value.to_constr v with
   | Some c ->
     begin
@@ -356,7 +355,7 @@ let coerce_to_quantified_hypothesis sigma v =
 
 (* Quantified named or numbered hypothesis or hypothesis in context *)
 (* (as in Inversion) *)
-let coerce_to_decl_or_quant_hyp env sigma v =
+let coerce_to_decl_or_quant_hyp sigma v =
   if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
   else
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 56f881684..d2ae92f6c 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -51,12 +51,12 @@ val coerce_to_constr_context : Value.t -> constr
 
 val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t
 
-val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t
+val coerce_to_ident_not_fresh : Evd.evar_map -> Value.t -> Id.t
 
-val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
+val coerce_to_intro_pattern : Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
 
 val coerce_to_intro_pattern_naming :
-  Environ.env -> Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
+  Evd.evar_map -> Value.t -> Namegen.intro_pattern_naming_expr
 
 val coerce_to_hint_base : Value.t -> string
 
@@ -64,7 +64,7 @@ val coerce_to_int : Value.t -> int
 
 val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders
 
-val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr
+val coerce_to_uconstr : Value.t -> Ltac_pretype.closed_glob_constr
 
 val coerce_to_closed_constr : Environ.env -> Value.t -> constr
 
@@ -74,17 +74,17 @@ val coerce_to_evaluable_ref :
 val coerce_to_constr_list : Environ.env -> Value.t -> constr list
 
 val coerce_to_intro_pattern_list :
-  ?loc:Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
+  ?loc:Loc.t -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
 
 val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t
 
 val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list
 
-val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> GlobRef.t
+val coerce_to_reference : Evd.evar_map -> Value.t -> GlobRef.t
 
 val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis
 
-val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis
+val coerce_to_decl_or_quant_hyp : Evd.evar_map -> Value.t -> quantified_hypothesis
 
 val coerce_to_int_or_var_list : Value.t -> int Locus.or_var list
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9d1cc1643..d9ac96d89 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -312,11 +312,11 @@ let interp_name ist env sigma = function
   | Name id -> Name (interp_ident ist env sigma id)
 
 let interp_intro_pattern_var loc ist env sigma id =
-  try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id)
+  try try_interp_ltac_var (coerce_to_intro_pattern sigma) ist (Some (env,sigma)) (make ?loc id)
   with Not_found -> IntroNaming (IntroIdentifier id)
 
 let interp_intro_pattern_naming_var loc ist env sigma id =
-  try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id)
+  try try_interp_ltac_var (coerce_to_intro_pattern_naming sigma) ist (Some (env,sigma)) (make ?loc id)
   with Not_found -> IntroIdentifier id
 
 let interp_int ist ({loc;v=id} as locid) =
@@ -357,7 +357,7 @@ let interp_hyp_list ist env sigma l =
 let interp_reference ist env sigma = function
   | ArgArg (_,r) -> r
   | ArgVar {loc;v=id} ->
-    try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id)
+    try try_interp_ltac_var (coerce_to_reference sigma) ist (Some (env,sigma)) (make ?loc id)
     with Not_found ->
       try
         VarRef (get_id (Environ.lookup_named id env))
@@ -451,7 +451,7 @@ let default_fresh_id = Id.of_string "H"
 
 let interp_fresh_id ist env sigma l =
   let extract_ident ist env sigma id =
-    try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma)
+    try try_interp_ltac_var (coerce_to_ident_not_fresh sigma)
                             ist (Some (env,sigma)) (make id)
     with Not_found -> id in
   let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in
@@ -474,7 +474,7 @@ let interp_fresh_id ist env sigma l =
 (* Extract the uconstr list from lfun *)
 let extract_ltac_constr_context ist env sigma =
   let add_uconstr id v map =
-    try Id.Map.add id (coerce_to_uconstr env v) map
+    try Id.Map.add id (coerce_to_uconstr v) map
     with CannotCoerceTo _ -> map
   in
   let add_constr id v map =
@@ -799,7 +799,7 @@ and interp_or_and_intro_pattern ist env sigma = function
 
 and interp_intro_pattern_list_as_list ist env sigma = function
   | [{loc;v=IntroNaming (IntroIdentifier id)}] as l ->
-      (try sigma, coerce_to_intro_pattern_list ?loc env sigma (Id.Map.find id ist.lfun)
+      (try sigma, coerce_to_intro_pattern_list ?loc sigma (Id.Map.find id ist.lfun)
        with Not_found | CannotCoerceTo _ ->
          List.fold_left_map (interp_intro_pattern ist env) sigma l)
   | l -> List.fold_left_map (interp_intro_pattern ist env) sigma l
@@ -842,7 +842,7 @@ let interp_declared_or_quantified_hypothesis ist env sigma = function
   | AnonHyp n -> AnonHyp n
   | NamedHyp id ->
       try try_interp_ltac_var
-            (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id)
+            (coerce_to_decl_or_quant_hyp sigma) ist (Some (env,sigma)) (make id)
       with Not_found -> NamedHyp id
 
 let interp_binding ist env sigma {loc;v=(b,c)} =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 6f4138828..e14c4e2ec 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -38,15 +38,9 @@ open OmegaSolver
 
 (* Added by JCF, 09/03/98 *)
 
-let elim_id id =
-  Proofview.Goal.enter begin fun gl ->
-    simplest_elim (mkVar id)
-  end
-let resolve_id id = Proofview.Goal.enter begin fun gl ->
-  apply (mkVar id)
-end
+let elim_id id = simplest_elim (mkVar id)
 
-let timing timer_name f arg = f arg
+let resolve_id id = apply (mkVar id)
 
 let display_time_flag = ref false
 let display_system_flag = ref false