diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index f49b1660b8..7eeee7ee07 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1064,7 +1064,7 @@ 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 subst) data.pat in + let pat' = Option.Smart.map (subst_pattern (Global.env()) 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) -> |