diff options
| author | Matthieu Sozeau | 2015-09-30 18:30:03 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:12 +0200 |
| commit | 2dc998e153922fffa907342871917963ad421e45 (patch) | |
| tree | a65f46be367f746e88f2d35387c3d8eead9fa13e | |
| parent | 4b51494ef6fee2301766fb4a44020dc2ad95799f (diff) | |
Univs: fix evar_map handling in Hint processing.
| -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 ead26e964f..a72c6ab51e 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 48b4505327..a7eae667d0 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 |