diff options
| author | Maxime Dénès | 2019-04-05 10:02:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:44 +0200 |
| commit | 61d53a17c594de1ea37b37f6215319d996ec31ea (patch) | |
| tree | 83c55ef28fd53d6f8af965e0c87ee6a168f90bb4 /tactics | |
| parent | 69c31d24fc8d058070cc7cadc1df28bfac7f6497 (diff) | |
Remove calls to Global.env in Patternops
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 4 | ||||
| -rw-r--r-- | tactics/redexpr.ml | 4 |
2 files changed, 6 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 7eeee7ee07..3854606afa 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 7ff88bb4b7..447b908a1d 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 |