diff options
| -rw-r--r-- | tactics/extratactics.ml4 | 8 | ||||
| -rw-r--r-- | tactics/hints.ml | 4 |
2 files changed, 6 insertions, 6 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index ead26e964..a72c6ab51 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -268,11 +268,9 @@ let add_rewrite_hint bases ort t lcsr = let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in let ctx = - if poly then - Evd.evar_universe_context_set Univ.UContext.empty ctx - else - let cstrs = Evd.evar_universe_context_constraints ctx in - (Global.add_constraints cstrs; Univ.ContextSet.empty) + let ctx = Evd.evar_universe_context_set Univ.UContext.empty ctx in + if poly then ctx + else (Global.push_context_set ctx; Univ.ContextSet.empty) in Constrexpr_ops.constr_loc ce, (c, ctx), ort, t in let eqs = List.map f lcsr in diff --git a/tactics/hints.ml b/tactics/hints.ml index 48b450532..a7eae667d 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1085,8 +1085,10 @@ let prepare_hint check env init (sigma,c) = let interp_hints poly = fun h -> + let env = (Global.env()) in + let sigma = Evd.from_env env in let f c = - let evd,c = Constrintern.interp_open_constr (Global.env()) Evd.empty c in + let evd,c = Constrintern.interp_open_constr env sigma c in prepare_hint true (Global.env()) Evd.empty (evd,c) in let fref r = let gr = global_with_alias r in |