From f8bbe2c1125593eb57ba01b903d5954e12bfb006 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 18 Jun 2008 14:17:57 +0000
Subject: meilleur gestion de la fonction de "cache" des alias (declaremods),
 et correction d'un bug sur Import/Export module.

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

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 4a2dd9afcd..83fc398e7e 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -164,7 +164,7 @@ and check_with_aux_mod env mtb with_decl now =
 	      in
 		if now then 
 		  let mp' = scrape_alias mp env' in
-		  let up_subst = update_subst_alias mtb'.typ_alias (map_mp (mp_rec [id]) mp') in
+		  let up_subst = update_subst mtb'.typ_alias (map_mp (mp_rec [id]) mp') in
 		    cst, (join (map_mp (mp_rec [id]) mp') up_subst)
 		else
 		cst,empty_subst
@@ -186,7 +186,7 @@ and check_with_aux_mod env mtb with_decl now =
 			if now then 
 			  let mtb' = lookup_modtype mp env' in
 			  let mp' = scrape_alias mp env' in
-			  let up_subst = update_subst_alias 
+			  let up_subst = update_subst 
 			    mtb'.typ_alias (map_mp (mp_rec (List.rev (id::idl))) mp') in
 			    cst, (join (map_mp (mp_rec (List.rev (id::idl))) mp') up_subst)
 		else
-- 
cgit v1.2.3