Univs: fix bug #3978: carry around the universe context used to

typecheck with definitions and thread it accordingly when typechecking
module expressions.

1 files changed, 2 insertions, 2 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 392e667b8..83be03ffd 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -177,9 +177,9 @@ let subst_with_body sub = function
   |WithMod(id,mp) as orig ->
     let mp' = subst_mp sub mp in
     if mp==mp' then orig else WithMod(id,mp')
-  |WithDef(id,c) as orig ->
+  |WithDef(id,(c,ctx)) as orig ->
     let c' = subst_mps sub c in
-    if c==c' then orig else WithDef(id,c')
+    if c==c' then orig else WithDef(id,(c',ctx))
 
 let rec subst_structure sub do_delta sign =
   let subst_body ((l,body) as orig) = match body with