From 7d2ac586a0f7dc0a497d1c94a9320a11c3e1f3c5 Mon Sep 17 00:00:00 2001 From: soubiran Date: Mon, 9 Jun 2008 19:21:03 +0000 Subject: Ajout d'un comportement special du sous-typage pour les constantes opaques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11082 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/safe_typing.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'kernel/safe_typing.ml') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a3df35ad5..c39a42646 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -314,10 +314,11 @@ let add_module l me senv = let add_alias l mp senv = check_label l senv.labset; let mp' = MPdot(senv.modinfo.modpath, l) in - (* we get all alias substitutions that comes from mp *) - let _,sub = translate_struct_entry senv.env (MSEident mp) in + (* we get all updated alias substitutions that comes from mp *) + let _,sub = Modops.update_subst senv.env (lookup_module mp senv.env) mp in (* we add the new one *) let mp1 = scrape_alias mp senv.env in + let sub = update_subst sub (map_mp mp' mp) in let sub = join (map_mp mp' mp1) sub in let env' = register_alias mp' mp senv.env in mp', { old = senv.old; -- cgit v1.2.3