diff options
Diffstat (limited to 'tactics/extratactics.ml4')
| -rw-r--r-- | tactics/extratactics.ml4 | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index af0870bc92..ead26e964f 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -262,7 +262,8 @@ TACTIC EXTEND rewrite_star (* Hint Rewrite *) let add_rewrite_hint bases ort t lcsr = - let env = Global.env() and sigma = Evd.empty in + let env = Global.env() in + let sigma = Evd.from_env env in let poly = Flags.is_universe_polymorphism () in let f ce = let c, ctx = Constrintern.interp_constr env sigma ce in @@ -490,7 +491,9 @@ let inTransitivity : bool * constr -> obj = (* Main entry points *) let add_transitivity_lemma left lem = - let lem',ctx (*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty lem in + let env = Global.env () in + let sigma = Evd.from_env env in + let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in add_anonymous_leaf (inTransitivity (left,lem')) (* Vernacular syntax *) |