diff options
Diffstat (limited to 'tactics/redexpr.ml')
| -rw-r--r-- | tactics/redexpr.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index aabfae444e..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 subs) + (Patternops.subst_pattern env sigma subs) let inReduction : bool * string * red_expr -> obj = declare_object |