From 44cedab7be5a44a01d467fbd2dba24400d575206 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Tue, 5 Feb 2008 13:28:06 +0000
Subject: Correction d'un bug sur les substitutions:

Require Import FSets FSetAVL.
Module M:=FSetAVL.Make Z_as_OT. (* ... uncaught exception Not_found *)




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

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 44907fd589..dffdb9e6fc 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -545,7 +545,7 @@ let rec get_modtype_substobjs env = function
 		 Modops.resolver_of_environment farg_id farg_b mp env in
 		 (* application outside the kernel, only for substitutive
                     objects (that are all non-logical objects) *)
-		 (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs)
+		 (join subst (add_mbid mbid mp (Some resolve) empty_subst), mbids, msid, objs)
 	   | [] -> match mexpr with
 	       | MSEident _  -> error "Application of a non-functor"
 	       | _ -> error "Application of a functor with too few arguments")
@@ -849,7 +849,7 @@ let rec get_module_substobjs env = function
                Modops.resolver_of_environment farg_id farg_b mp env in
                (* application outside the kernel, only for substitutive
                   objects (that are all non-logical objects) *)
-	       (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs)
+	       (join subst (add_mbid mbid mp (Some resolve) empty_subst), mbids, msid, objs)
 	   | [] -> match mexpr with
 	       | MSEident _  -> error "Application of a non-functor"
 	       | _ -> error "Application of a functor with too few arguments")
-- 
cgit v1.2.3