From 4784a0690e760e48d5c3566b01df500d321c14eb Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 8 Nov 2002 11:00:41 +0000
Subject: Correction bug PR#222

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3224 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/declaremods.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 397104d7b5..6cae78bba4 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -475,10 +475,10 @@ let end_module id =
   let substituted = subst_substobjs dir mp substobjs in
   let node = in_module (None,substobjs,substituted) in
   let objects = 
-    if keep = [] then 
-      special@[node]
+    if keep = [] || mbids <> [] then 
+      special@[node]   (* no keep objects or we are defining a functor *)
     else
-      special@[node;in_modkeep keep]
+      special@[node;in_modkeep keep]   (* otherwise *)
   in
   let newoname = Lib.add_leaves id objects in
 
-- 
cgit v1.2.3