diff options
| author | Maxime Dénès | 2019-04-04 21:06:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:43 +0200 |
| commit | bf5f0520cf105afb048c6eac5d6de1d3e1a719df (patch) | |
| tree | dfc7afd2f394958a81c5ce33d1422f72b7e6b36b /plugins/ltac | |
| parent | 3b980d937b5adfbae472ed8a13748a451fdf3450 (diff) | |
Remove one call to Global.env in Detyping
One other call still remains, but will require to refactor some
section-handling code.
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/tacsubst.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml index caaa547a07..8fb238aecb 100644 --- a/plugins/ltac/tacsubst.ml +++ b/plugins/ltac/tacsubst.ml @@ -30,7 +30,7 @@ let subst_quantified_hypothesis _ x = x let subst_declared_or_quantified_hypothesis _ x = x let subst_glob_constr_and_expr subst (c, e) = - (Detyping.subst_glob_constr subst c, e) + (Detyping.subst_glob_constr (Global.env()) subst c, e) let subst_glob_constr = subst_glob_constr_and_expr (* shortening *) @@ -99,7 +99,7 @@ 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 subst p) + (bvars,subst_glob_constr subst c,subst_pattern (Global.env()) subst p) let subst_redexp subst = Redops.map_red_expr_gen |