From 61d53a17c594de1ea37b37f6215319d996ec31ea Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Fri, 5 Apr 2019 10:02:18 +0200 Subject: [PATCH] Remove calls to Global.env in Patternops --- plugins/ltac/tacsubst.ml | 4 +++- pretyping/patternops.ml | 48 +++++++++++++++++++--------------------- pretyping/patternops.mli | 2 +- tactics/hints.ml | 4 +++- tactics/redexpr.ml | 4 +++- 5 files changed, 33 insertions(+), 29 deletions(-) diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 8fb238aecba9..e617f3d45ec7 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -99,7 +99,9 @@ let subst_evaluable subst = let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c) let subst_glob_constr_or_pattern subst (bvars,c,p) = - (bvars,subst_glob_constr subst c,subst_pattern (Global.env()) subst p) + let env = Global.env () in + let sigma = Evd.from_env env in + (bvars,subst_glob_constr subst c,subst_pattern env sigma subst p) let subst_redexp subst = Redops.map_red_expr_gen diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 9ce63e420762..b29afd1fd2b1 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -280,66 +280,64 @@ let rec liftn_pattern k n = function let lift_pattern k = liftn_pattern k 1 -let rec subst_pattern env subst pat = +let rec subst_pattern env sigma subst pat = match pat with | PRef ref -> let ref',t = subst_global subst ref in if ref' == ref then pat else (match t with | None -> PRef ref' | Some t -> - let env = Global.env () in - let evd = Evd.from_env env in - pattern_of_constr env evd t.Univ.univ_abstracted_value) + pattern_of_constr env sigma t.Univ.univ_abstracted_value) | PVar _ | PEvar _ | PRel _ | PInt _ -> pat | PProj (p,c) -> let p' = Projection.map (subst_mind subst) p in - let c' = subst_pattern env subst c in + let c' = subst_pattern env sigma subst c in if p' == p && c' == c then pat else PProj(p',c') | PApp (f,args) -> - let f' = subst_pattern env subst f in - let args' = Array.Smart.map (subst_pattern env subst) args in + let f' = subst_pattern env sigma subst f in + let args' = Array.Smart.map (subst_pattern env sigma subst) args in if f' == f && args' == args then pat else PApp (f',args') | PSoApp (i,args) -> - let args' = List.Smart.map (subst_pattern env subst) args in + let args' = List.Smart.map (subst_pattern env sigma subst) args in if args' == args then pat else PSoApp (i,args') | PLambda (name,c1,c2) -> - let c1' = subst_pattern env subst c1 in - let c2' = subst_pattern env subst c2 in + let c1' = subst_pattern env sigma subst c1 in + let c2' = subst_pattern env sigma subst c2 in if c1' == c1 && c2' == c2 then pat else PLambda (name,c1',c2') | PProd (name,c1,c2) -> - let c1' = subst_pattern env subst c1 in - let c2' = subst_pattern env subst c2 in + let c1' = subst_pattern env sigma subst c1 in + let c2' = subst_pattern env sigma subst c2 in if c1' == c1 && c2' == c2 then pat else PProd (name,c1',c2') | PLetIn (name,c1,t,c2) -> - let c1' = subst_pattern env subst c1 in - let t' = Option.Smart.map (subst_pattern env subst) t in - let c2' = subst_pattern env subst c2 in + let c1' = subst_pattern env sigma subst c1 in + let t' = Option.Smart.map (subst_pattern env sigma subst) t in + let c2' = subst_pattern env sigma subst c2 in if c1' == c1 && t' == t && c2' == c2 then pat else PLetIn (name,c1',t',c2') | PSort _ | PMeta _ -> pat | PIf (c,c1,c2) -> - let c' = subst_pattern env subst c in - let c1' = subst_pattern env subst c1 in - let c2' = subst_pattern env subst c2 in + let c' = subst_pattern env sigma subst c in + let c1' = subst_pattern env sigma subst c1 in + let c2' = subst_pattern env sigma subst c2 in if c' == c && c1' == c1 && c2' == c2 then pat else PIf (c',c1',c2') | PCase (cip,typ,c,branches) -> let ind = cip.cip_ind in let ind' = Option.Smart.map (subst_ind subst) ind in let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in - let typ' = subst_pattern env subst typ in - let c' = subst_pattern env subst c in + let typ' = subst_pattern env sigma subst typ in + let c' = subst_pattern env sigma subst c in let subst_branch ((i,n,c) as br) = - let c' = subst_pattern env subst c in + let c' = subst_pattern env sigma subst c in if c' == c then br else (i,n,c') in let branches' = List.Smart.map subst_branch branches in @@ -347,13 +345,13 @@ let rec subst_pattern env subst pat = then pat else PCase(cip', typ', c', branches') | PFix (lni,(lna,tl,bl)) -> - let tl' = Array.Smart.map (subst_pattern env subst) tl in - let bl' = Array.Smart.map (subst_pattern env subst) bl in + let tl' = Array.Smart.map (subst_pattern env sigma subst) tl in + let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in if bl' == bl && tl' == tl then pat else PFix (lni,(lna,tl',bl')) | PCoFix (ln,(lna,tl,bl)) -> - let tl' = Array.Smart.map (subst_pattern env subst) tl in - let bl' = Array.Smart.map (subst_pattern env subst) bl in + let tl' = Array.Smart.map (subst_pattern env sigma subst) tl in + let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in if bl' == bl && tl' == tl then pat else PCoFix (ln,(lna,tl',bl')) diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 90a536e78095..3821fbf1a035 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -21,7 +21,7 @@ val constr_pattern_eq : constr_pattern -> constr_pattern -> bool val occur_meta_pattern : constr_pattern -> bool -val subst_pattern : Environ.env -> substitution -> constr_pattern -> constr_pattern +val subst_pattern : Environ.env -> Evd.evar_map -> substitution -> constr_pattern -> constr_pattern val noccurn_pattern : int -> constr_pattern -> bool diff --git a/tactics/hints.ml b/tactics/hints.ml index 7eeee7ee07dd..3854606afa06 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1064,7 +1064,9 @@ let subst_autohint (subst, obj) = in let subst_hint (k,data as hint) = let k' = Option.Smart.map subst_key k in - let pat' = Option.Smart.map (subst_pattern (Global.env()) subst) data.pat in + let env = Global.env () in + let sigma = Evd.from_env env in + let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in let code' = match data.code.obj with | Res_pf (c,t,ctx) -> diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index 7ff88bb4b71b..447b908a1d4c 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -259,10 +259,12 @@ let subst_mps subst c = EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c)) let subst_red_expr subs = + let env = Global.env () in + let sigma = Evd.from_env env in Redops.map_red_expr_gen (subst_mps subs) (Mod_subst.subst_evaluable_reference subs) - (Patternops.subst_pattern (Global.env()) subs) + (Patternops.subst_pattern env sigma subs) let inReduction : bool * string * red_expr -> obj = declare_object