From f07768cd1b8373801ec5375ee79c800f98403828 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Thu, 18 Dec 2008 15:53:23 +0000
Subject: Correction d'un bug causant un Not_found dans la contrib FSet.

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

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 4fc9d10b67..76487af686 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -659,8 +659,8 @@ let rec get_modtype_substobjs env = function
 		 (* application outside the kernel, only for substitutive
                     objects (that are all non-logical objects) *)
 		((join 
-		    (join subst (map_mbid mbid mp (Some resolve)))
-		       sub3)
+		    (join subst sub3)
+		       (map_mbid mbid mp (Some resolve)))
 		       , mbids, msid, objs)
 	   | [] -> match mexpr with
 	       | MSEident _  -> error "Application of a non-functor"
@@ -966,8 +966,8 @@ let rec get_module_substobjs env = function
 		 (* application outside the kernel, only for substitutive
                     objects (that are all non-logical objects) *)
 		((join 
-		    (join subst (map_mbid mbid mp (Some resolve)))
-		       sub3)
+		    (join subst sub3)
+		       (map_mbid mbid mp (Some resolve)))
 		       , mbids, msid, objs)
 	   | [] -> match mexpr with
 	       | MSEident _  -> error "Application of a non-functor"
-- 
cgit v1.2.3