From 5c603ebd99e4e8e7abb8b2036a6ffac5b19f66cf Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <matthieu.sozeau@inria.fr>
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.

---
 kernel/modops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/modops.ml')

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
-- 
cgit v1.2.3