From 866c41b9720413e00194ba7addb9c4277e114890 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 27 May 2015 11:43:11 +0200
Subject: Fix bug #4159 Some asynchronous constraints between initial universes
 and the ones at the end of a proof were forgotten. Also add a message to
 print universes indicating if all the constraints are processed already or
 not.

---
 interp/modintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/modintern.ml b/interp/modintern.ml
index bf0b2f9800..35e731137f 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -62,7 +62,7 @@ let transl_with_decl env = function
       WithMod (fqid,lookup_module qid)
   | CWith_Definition ((_,fqid),c) ->
     let c, ectx = interp_constr env (Evd.from_env env) c in
-    let ctx = Univ.ContextSet.to_context (Evd.evar_universe_context_set ectx) in
+    let ctx = Evd.evar_context_universe_context ectx in
       WithDef (fqid,(c,ctx))
 
 let loc_of_module = function
-- 
cgit v1.2.3