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 /plugins | |
| parent | 69c31d24fc8d058070cc7cadc1df28bfac7f6497 (diff) | |
Remove calls to Global.env in Patternops
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index 8fb238aecb..e617f3d45e 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 |