From 86b28df4c6029d43a0f12ab7c2d85cc13f4f60f1 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 6 Jun 2008 16:03:45 +0000
Subject: ajout d'un printer pour les contraintes d'univers + correction d'un
 bug sur les notations dans les alias de module.

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

(limited to 'library')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 0b0483a853..0bb74f74a6 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -355,8 +355,9 @@ let subst_module ((sp,kn),subst,(entry,substobjs,_)) =
 let subst_module_alias ((sp,kn),subst,(entry,substobjs,_)) =
   let dir,mp = dir_of_sp sp, mp_of_kn kn in
   let (sub,mbids,msid,objs) = substobjs in
-  let sub = update_subst_alias subst (map_msid msid mp) in
-  let subst' = join sub subst in
+  let sub' = update_subst_alias subst (map_msid msid mp) in
+  let subst' = join sub' subst in
+  let subst' = join sub subst' in
   (* substitutive_objects get the new substitution *)
   let substobjs = (subst',mbids,msid,objs) in
   (* if we are not a functor - calculate substitued.
-- 
cgit v1.2.3