From 2dc998e153922fffa907342871917963ad421e45 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 30 Sep 2015 18:30:03 +0200
Subject: Univs: fix evar_map handling in Hint processing.

---
 tactics/extratactics.ml4 | 8 +++-----
 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
-- 
cgit v1.2.3