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

1 files changed, 3 insertions, 2 deletions

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;