From 5c603ebd99e4e8e7abb8b2036a6ffac5b19f66cf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 12 Feb 2015 22:41:40 +0100
Subject: Univs: fix bug #3978: carry around the universe context used to
 typecheck with definitions and thread it accordingly when typechecking module
 expressions.

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

(limited to 'interp')

diff --git a/interp/modintern.ml b/interp/modintern.ml
index fdc6e609bc..bf0b2f9800 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -61,7 +61,9 @@ let transl_with_decl env = function
   | CWith_Module ((_,fqid),qid) ->
       WithMod (fqid,lookup_module qid)
   | CWith_Definition ((_,fqid),c) ->
-      WithDef (fqid,fst (interp_constr env Evd.empty c)) (*FIXME*)
+    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
+      WithDef (fqid,(c,ctx))
 
 let loc_of_module = function
   | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc
-- 
cgit v1.2.3