From 680492f83b2a4f336f639def7c59f55cf8469395 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 1 Sep 2017 15:53:24 +0200 Subject: Taccoerce: remove various unused arguments. --- plugins/ltac/taccoerce.ml | 23 +++++++++++------------ plugins/ltac/taccoerce.mli | 14 +++++++------- plugins/ltac/tacinterp.ml | 14 +++++++------- 3 files changed, 25 insertions(+), 26 deletions(-) (limited to 'plugins') 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)} = -- cgit v1.2.3