From 2dbe106c09b60690b87e31e58d505b1f4e05b57f Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Fri, 11 May 2007 17:00:58 +0000
Subject: Processor integers + Print assumption (see coqdev mailing list for
 the details).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/mod_typing.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index ad5df805ba..93d01f12aa 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -170,7 +170,8 @@ and translate_module env  me =
 	  mod_user_type = Some mtb;
 	  mod_type = mtb;
 	  mod_equiv = None;
-	  mod_constraints = Constraint.empty }
+	  mod_constraints = Constraint.empty;
+	  mod_retroknowledge = [] } 
     | Some mexpr, _ -> 
 	let meq_o = (* do we have a transparent module ? *)
 	  try       (* TODO: transparent field in module_entry *)
@@ -193,7 +194,11 @@ and translate_module env  me =
 	    mod_user_type = mod_user_type;
 	    mod_expr = Some meb;
 	    mod_equiv = meq_o;
-	    mod_constraints = cst }
+	    mod_constraints = cst;
+	    mod_retroknowledge = []} (* spiwack: not so sure about that. It may
+					cause a bug when closing nested modules.
+					If it does, I don't really know how to
+					fix the bug.*)
 
 (* translate_mexpr : env -> module_expr -> module_expr_body * module_type_body *)
 and translate_mexpr env mexpr = match mexpr with
-- 
cgit v1.2.3