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
---
 contrib/extraction/modutil.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index eb5c274502..519565888a 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -49,7 +49,10 @@ let rec subst_module sub mb =
 	 mod_type=mtb'; 
 	 mod_user_type=mtb''; 
 	 mod_equiv=mpo'; 
-	 mod_constraints=mb.mod_constraints }
+	 mod_constraints=mb.mod_constraints;
+         mod_retroknowledge=[] } (* spiwack: since I'm lazy and it's unused at 
+				    this point. I forget about retroknowledge, 
+				    this may need a change later *)
 
 and subst_meb sub = function 
   | MEBident mp -> MEBident (subst_mp sub mp) 
-- 
cgit v1.2.3