From 07f4e6b07775052cc1c5dc34cdfa7ad4eacfa94f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sun, 4 Oct 2015 14:50:45 +0200
Subject: Fix bug #4354: interpret hints in the right env and sigma.

---
 pretyping/evd.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 842b87c57e..4e0b6f75e7 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -312,7 +312,10 @@ let union_evar_universe_context ctx ctx' =
     let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in
     let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local)
 			       (Univ.ContextSet.levels ctx.uctx_local) in
-    let declarenew g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g in	
+    let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in
+    let declarenew g =
+      Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g
+    in
     let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in
       { uctx_names = (names, names_rev);
 	uctx_local = local;
-- 
cgit v1.2.3


From df9caebb04fb681ec66b79c41ae01918cd2336de Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 6 Oct 2015 09:58:20 +0200
Subject: Univs (pretyping): call vm_compute/native_compute with the current
 universe graph

---
 pretyping/pretyping.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f18657da82..2efd8fe413 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -903,7 +903,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
 	      if not (occur_existential cty || occur_existential tval) then
 		begin 
-		  try 
+		  try
+		    let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in 
 		    ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
 		  with Reduction.NotConvertible -> 
 		    error_actual_type_loc loc env !evdref cj tval 
@@ -915,6 +916,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
  	    let cj = pretype empty_tycon env evdref lvar c in
 	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
             let evars = Nativenorm.evars_of_evar_map !evdref in
+	    let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in 
             begin
               try
                 ignore (Nativeconv.native_conv Reduction.CUMUL evars env cty tval); cj
-- 
cgit v1.2.3