fixed bug with aliases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10896 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 155 insertions, 314 deletions

diff --git a/checker/.depend b/checker/.depend
index dade1591b..09ab6bdd1 100644
--- a/checker/.depend
+++ b/checker/.depend
@@ -1,116 +1,58 @@
-checker.cmo: ../lib/util.cmi ../kernel/univ.cmi type_errors.cmi \
-    /usr/lib/ocaml/camlp4/token.cmi ../kernel/term.cmi ../lib/system.cmi \
-    /usr/lib/ocaml/camlp4/stdpp.cmi safe_typing.cmi ../lib/pp.cmi \
-    ../kernel/names.cmi indtypes.cmi ../lib/flags.cmi declarations.cmi \
-    ../config/coq_config.cmi check_stat.cmi check.cmo 
-checker.cmx: ../lib/util.cmx ../kernel/univ.cmx type_errors.cmx \
-    /usr/lib/ocaml/camlp4/token.cmi ../kernel/term.cmx ../lib/system.cmx \
-    /usr/lib/ocaml/camlp4/stdpp.cmi safe_typing.cmx ../lib/pp.cmi \
-    ../kernel/names.cmx indtypes.cmx ../lib/flags.cmx declarations.cmx \
-    ../config/coq_config.cmx check_stat.cmx check.cmx 
-check.cmo: ../lib/util.cmi ../lib/system.cmi safe_typing.cmi ../lib/pp.cmi \
-    ../kernel/names.cmi ../lib/flags.cmi 
-check.cmx: ../lib/util.cmx ../lib/system.cmx safe_typing.cmx ../lib/pp.cmi \
-    ../kernel/names.cmx ../lib/flags.cmx 
-check_stat.cmo: ../lib/util.cmi ../kernel/term.cmi ../lib/system.cmi \
-    safe_typing.cmi ../lib/pp.cmi ../kernel/names.cmi indtypes.cmi \
-    ../lib/flags.cmi ../kernel/environ.cmi declarations.cmi check_stat.cmi 
-check_stat.cmx: ../lib/util.cmx ../kernel/term.cmx ../lib/system.cmx \
-    safe_typing.cmx ../lib/pp.cmi ../kernel/names.cmx indtypes.cmx \
-    ../lib/flags.cmx ../kernel/environ.cmx declarations.cmx check_stat.cmi 
-closure.cmo: ../lib/util.cmi ../kernel/term.cmi ../lib/pp.cmi \
-    ../kernel/names.cmi ../kernel/esubst.cmi ../kernel/environ.cmi \
-    closure.cmi 
-closure.cmx: ../lib/util.cmx ../kernel/term.cmx ../lib/pp.cmi \
-    ../kernel/names.cmx ../kernel/esubst.cmx ../kernel/environ.cmx \
-    closure.cmi 
-closure.cmi: ../kernel/term.cmi ../lib/pp.cmi ../kernel/names.cmi \
-    ../kernel/esubst.cmi ../kernel/environ.cmi 
-declarations.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \
-    ../lib/rtree.cmi ../lib/option.cmi ../kernel/names.cmi declarations.cmi 
-declarations.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \
-    ../lib/rtree.cmx ../lib/option.cmx ../kernel/names.cmx declarations.cmi 
-declarations.cmi: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \
-    ../lib/rtree.cmi ../kernel/names.cmi 
-environ.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \
-    ../kernel/names.cmi declarations.cmi 
-environ.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \
-    ../kernel/names.cmx declarations.cmx 
-indtypes.cmo: ../lib/util.cmi ../kernel/univ.cmi typeops.cmi \
-    ../kernel/term.cmi ../lib/rtree.cmi reduction.cmi ../lib/pp.cmi \
-    ../kernel/names.cmi inductive.cmi ../lib/flags.cmi ../kernel/environ.cmi \
+checker.cmo: type_errors.cmi term.cmo safe_typing.cmi indtypes.cmi \
+    declarations.cmi check_stat.cmi check.cmo 
+checker.cmx: type_errors.cmx term.cmx safe_typing.cmx indtypes.cmx \
+    declarations.cmx check_stat.cmx check.cmx 
+check.cmo: safe_typing.cmi 
+check.cmx: safe_typing.cmx 
+check_stat.cmo: term.cmo safe_typing.cmi indtypes.cmi environ.cmo \
+    declarations.cmi check_stat.cmi 
+check_stat.cmx: term.cmx safe_typing.cmx indtypes.cmx environ.cmx \
+    declarations.cmx check_stat.cmi 
+closure.cmo: term.cmo environ.cmo closure.cmi 
+closure.cmx: term.cmx environ.cmx closure.cmi 
+closure.cmi: term.cmo environ.cmo 
+declarations.cmo: term.cmo declarations.cmi 
+declarations.cmx: term.cmx declarations.cmi 
+declarations.cmi: term.cmo 
+environ.cmo: term.cmo declarations.cmi 
+environ.cmx: term.cmx declarations.cmx 
+indtypes.cmo: typeops.cmi term.cmo reduction.cmi inductive.cmi environ.cmo \
     declarations.cmi indtypes.cmi 
-indtypes.cmx: ../lib/util.cmx ../kernel/univ.cmx typeops.cmx \
-    ../kernel/term.cmx ../lib/rtree.cmx reduction.cmx ../lib/pp.cmi \
-    ../kernel/names.cmx inductive.cmx ../lib/flags.cmx ../kernel/environ.cmx \
+indtypes.cmx: typeops.cmx term.cmx reduction.cmx inductive.cmx environ.cmx \
     declarations.cmx indtypes.cmi 
-indtypes.cmi: ../kernel/univ.cmi typeops.cmi ../kernel/term.cmi ../lib/pp.cmi \
-    ../kernel/names.cmi ../kernel/environ.cmi declarations.cmi 
-inductive.cmo: ../lib/util.cmi ../kernel/univ.cmi type_errors.cmi \
-    ../kernel/term.cmi ../lib/rtree.cmi reduction.cmi ../kernel/names.cmi \
-    ../kernel/environ.cmi declarations.cmi inductive.cmi 
-inductive.cmx: ../lib/util.cmx ../kernel/univ.cmx type_errors.cmx \
-    ../kernel/term.cmx ../lib/rtree.cmx reduction.cmx ../kernel/names.cmx \
-    ../kernel/environ.cmx declarations.cmx inductive.cmi 
-inductive.cmi: ../kernel/univ.cmi ../kernel/term.cmi ../kernel/names.cmi \
-    ../kernel/environ.cmi declarations.cmi 
+indtypes.cmi: typeops.cmi term.cmo environ.cmo declarations.cmi 
+inductive.cmo: type_errors.cmi term.cmo reduction.cmi environ.cmo \
+    declarations.cmi inductive.cmi 
+inductive.cmx: type_errors.cmx term.cmx reduction.cmx environ.cmx \
+    declarations.cmx inductive.cmi 
+inductive.cmi: term.cmo environ.cmo declarations.cmi 
 main.cmo: checker.cmo 
 main.cmx: checker.cmx 
-mod_checking.cmo: ../lib/util.cmi ../kernel/univ.cmi typeops.cmi \
-    ../kernel/term.cmi subtyping.cmi reduction.cmi ../lib/pp.cmi \
-    ../kernel/names.cmi modops.cmi inductive.cmi indtypes.cmi \
-    ../lib/flags.cmi ../kernel/environ.cmi declarations.cmi 
-mod_checking.cmx: ../lib/util.cmx ../kernel/univ.cmx typeops.cmx \
-    ../kernel/term.cmx subtyping.cmx reduction.cmx ../lib/pp.cmi \
-    ../kernel/names.cmx modops.cmx inductive.cmx indtypes.cmx \
-    ../lib/flags.cmx ../kernel/environ.cmx declarations.cmx 
-modops.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \
-    ../lib/pp.cmi ../lib/option.cmi ../kernel/names.cmi ../kernel/environ.cmi \
-    declarations.cmi modops.cmi 
-modops.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \
-    ../lib/pp.cmi ../lib/option.cmx ../kernel/names.cmx ../kernel/environ.cmx \
-    declarations.cmx modops.cmi 
-modops.cmi: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \
-    ../kernel/names.cmi ../kernel/environ.cmi declarations.cmi 
-reduction.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \
-    ../kernel/names.cmi ../kernel/esubst.cmi ../kernel/environ.cmi \
-    closure.cmi reduction.cmi 
-reduction.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \
-    ../kernel/names.cmx ../kernel/esubst.cmx ../kernel/environ.cmx \
-    closure.cmx reduction.cmi 
-reduction.cmi: ../kernel/term.cmi ../kernel/environ.cmi 
-safe_typing.cmo: validate.cmo ../lib/util.cmi ../lib/pp.cmi ../lib/option.cmi \
-    ../kernel/names.cmi modops.cmi mod_checking.cmo ../lib/flags.cmi \
-    ../kernel/environ.cmi declarations.cmi safe_typing.cmi 
-safe_typing.cmx: validate.cmx ../lib/util.cmx ../lib/pp.cmi ../lib/option.cmx \
-    ../kernel/names.cmx modops.cmx mod_checking.cmx ../lib/flags.cmx \
-    ../kernel/environ.cmx declarations.cmx safe_typing.cmi 
-safe_typing.cmi: ../kernel/term.cmi ../lib/system.cmi ../kernel/names.cmi \
-    ../kernel/environ.cmi declarations.cmi 
-subtyping.cmo: ../lib/util.cmi ../kernel/univ.cmi typeops.cmi \
-    ../kernel/term.cmi reduction.cmi ../lib/pp.cmi ../kernel/names.cmi \
-    modops.cmi inductive.cmi ../kernel/environ.cmi declarations.cmi \
-    subtyping.cmi 
-subtyping.cmx: ../lib/util.cmx ../kernel/univ.cmx typeops.cmx \
-    ../kernel/term.cmx reduction.cmx ../lib/pp.cmi ../kernel/names.cmx \
-    modops.cmx inductive.cmx ../kernel/environ.cmx declarations.cmx \
-    subtyping.cmi 
-subtyping.cmi: ../kernel/univ.cmi ../kernel/term.cmi ../kernel/environ.cmi \
-    declarations.cmi 
-term.cmo: ../lib/util.cmi ../kernel/univ.cmi ../lib/pp.cmi ../lib/option.cmi \
-    ../kernel/names.cmi ../kernel/esubst.cmi 
-term.cmx: ../lib/util.cmx ../kernel/univ.cmx ../lib/pp.cmi ../lib/option.cmx \
-    ../kernel/names.cmx ../kernel/esubst.cmx 
-type_errors.cmo: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi \
-    type_errors.cmi 
-type_errors.cmx: ../kernel/term.cmx ../kernel/names.cmx ../kernel/environ.cmx \
-    type_errors.cmi 
-type_errors.cmi: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi 
-typeops.cmo: ../lib/util.cmi ../kernel/univ.cmi type_errors.cmi \
-    ../kernel/term.cmi reduction.cmi ../kernel/names.cmi inductive.cmi \
-    ../kernel/environ.cmi declarations.cmi typeops.cmi 
-typeops.cmx: ../lib/util.cmx ../kernel/univ.cmx type_errors.cmx \
-    ../kernel/term.cmx reduction.cmx ../kernel/names.cmx inductive.cmx \
-    ../kernel/environ.cmx declarations.cmx typeops.cmi 
-typeops.cmi: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi \
-    declarations.cmi 
+mod_checking.cmo: typeops.cmi term.cmo subtyping.cmi reduction.cmi modops.cmi \
+    inductive.cmi indtypes.cmi environ.cmo declarations.cmi 
+mod_checking.cmx: typeops.cmx term.cmx subtyping.cmx reduction.cmx modops.cmx \
+    inductive.cmx indtypes.cmx environ.cmx declarations.cmx 
+modops.cmo: term.cmo environ.cmo declarations.cmi modops.cmi 
+modops.cmx: term.cmx environ.cmx declarations.cmx modops.cmi 
+modops.cmi: term.cmo environ.cmo declarations.cmi 
+reduction.cmo: term.cmo environ.cmo closure.cmi reduction.cmi 
+reduction.cmx: term.cmx environ.cmx closure.cmx reduction.cmi 
+reduction.cmi: term.cmo environ.cmo 
+safe_typing.cmo: validate.cmo modops.cmi mod_checking.cmo environ.cmo \
+    declarations.cmi safe_typing.cmi 
+safe_typing.cmx: validate.cmx modops.cmx mod_checking.cmx environ.cmx \
+    declarations.cmx safe_typing.cmi 
+safe_typing.cmi: term.cmo environ.cmo declarations.cmi 
+subtyping.cmo: typeops.cmi term.cmo reduction.cmi modops.cmi inductive.cmi \
+    environ.cmo declarations.cmi subtyping.cmi 
+subtyping.cmx: typeops.cmx term.cmx reduction.cmx modops.cmx inductive.cmx \
+    environ.cmx declarations.cmx subtyping.cmi 
+subtyping.cmi: term.cmo environ.cmo declarations.cmi 
+type_errors.cmo: term.cmo environ.cmo type_errors.cmi 
+type_errors.cmx: term.cmx environ.cmx type_errors.cmi 
+type_errors.cmi: term.cmo environ.cmo 
+typeops.cmo: type_errors.cmi term.cmo reduction.cmi inductive.cmi environ.cmo \
+    declarations.cmi typeops.cmi 
+typeops.cmx: type_errors.cmx term.cmx reduction.cmx inductive.cmx environ.cmx \
+    declarations.cmx typeops.cmi 
+typeops.cmi: term.cmo environ.cmo declarations.cmi 
diff --git a/checker/Makefile b/checker/Makefile
index 7567e78ff..2bcc9d365 100644
--- a/checker/Makefile
+++ b/checker/Makefile
@@ -10,15 +10,7 @@ OPTFLAGS=$(MLDIRS)
 CHECKERNAME=coqchk
 
 BINARIES=../bin/$(CHECKERNAME)$(EXE) ../bin/$(CHECKERNAME).opt$(EXE)
-
-MCHECKER:=\
-  $(COQSRC)/config/coq_config.cmo \
-  $(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \
-  $(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \
-  $(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \
-  $(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \
-  $(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \
-  $(COQSRC)/kernel/esubst.cmo term.cmo \
+MCHECKERLOCAL :=\
   declarations.cmo environ.cmo \
   closure.cmo reduction.cmo \
   type_errors.cmo \
@@ -29,15 +21,25 @@ validate.cmo \
   safe_typing.cmo check.cmo \
   check_stat.cmo checker.cmo
 
+MCHECKER:=\
+  $(COQSRC)/config/coq_config.cmo \
+  $(COQSRC)/lib/pp_control.cmo $(COQSRC)/lib/pp.cmo $(COQSRC)/lib/compat.cmo \
+  $(COQSRC)/lib/util.cmo $(COQSRC)/lib/option.cmo $(COQSRC)/lib/hashcons.cmo \
+  $(COQSRC)/lib/system.cmo $(COQSRC)/lib/flags.cmo \
+  $(COQSRC)/lib/predicate.cmo $(COQSRC)/lib/rtree.cmo \
+  $(COQSRC)/kernel/names.cmo $(COQSRC)/kernel/univ.cmo \
+  $(COQSRC)/kernel/esubst.cmo term.cmo \
+  $(MCHECKERLOCAL)
+
 all: $(BINARIES)
 
 byte : ../bin/$(CHECKERNAME)$(EXE)
 opt : ../bin/$(CHECKERNAME).opt$(EXE)
 
-check.cma: $(MCHECKER)
+check.cma: $(MCHECKERLOCAL)
 	ocamlc $(BYTEFLAGS) -a -o $@ $(MCHECKER)
 
-check.cmxa: $(MCHECKER:.cmo=.cmx)
+check.cmxa: $(MCHECKERLOCAL:.cmo=.cmx)
 	ocamlopt $(OPTFLAGS) -a -o $@ $(MCHECKER:.cmo=.cmx)
 
 ../bin/$(CHECKERNAME)$(EXE): check.cma
@@ -78,7 +80,7 @@ stats:
 
 
 depend::
-	ocamldep $(MLDIRS) *.ml* > .depend
+	ocamldep *.ml* > .depend
 
 clean::
 	rm -f *.cm* *.o *.a *~ $(BINARIES)
diff --git a/checker/check.ml b/checker/check.ml
index 646063519..7169d709f 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -342,10 +342,12 @@ let rec intern_library (dir, f) needed =
 and intern_mandatory_library (dir,_) needed =
   intern_library (try_locate_absolute_library dir) needed
 
-let recheck_library ~admit ~check =
-  let al = List.map (fun q -> fst(try_locate_qualified_library q)) admit in
-  let admit = List.fold_right library_dep al LibraryMap.empty in
-  let modl = List.map try_locate_qualified_library check in
+let recheck_library ~norec ~admit ~check =
+  let nrl = List.map (fun q -> fst(try_locate_qualified_library q)) norec in
+  let al =  List.map (fun q -> fst(try_locate_qualified_library q)) admit in
+  let admit = List.fold_right library_dep (nrl@al) LibraryMap.empty in
+  let admit = List.fold_right LibraryMap.remove nrl admit in
+  let modl = List.map try_locate_qualified_library (norec@check) in
   let needed = List.rev (List.fold_right intern_library modl []) in
   Flags.if_verbose msgnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
diff --git a/checker/checker.ml b/checker/checker.ml
index 832fe0663..0ae94444d 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -152,6 +152,10 @@ let admit_list = ref ([] : section_path list)
 let add_admit s =
   admit_list := path_of_string s :: !admit_list
 
+let norec_list = ref ([] : section_path list)
+let add_norec s =
+  norec_list := path_of_string s :: !norec_list
+
 let compile_list = ref ([] : section_path list)
 let add_compile s =
   compile_list := path_of_string s :: !compile_list
@@ -162,6 +166,7 @@ let add_compile s =
 
 let compile_files () =
   Check.recheck_library
+    ~norec:(List.rev !norec_list)
     ~admit:(List.rev !admit_list)
     ~check:(List.rev !compile_list) 
 
@@ -182,6 +187,7 @@ let print_usage_channel co command =
   -R dir coqdir          recursively map physical dir to logical coqdir 
 
   -admit module          load module and dependencies without checking
+  -norec module          check module but admit dependencies without checking
 
   -where                 print Coq's standard library location and exit
   -v                     print Coq version and exit
@@ -325,6 +331,9 @@ let parse_args() =
     | "-admit" :: s :: rem -> add_admit s; parse rem
     | "-admit" :: [] -> usage ()
 
+    | "-norec" :: s :: rem -> add_norec s; parse rem
+    | "-norec" :: [] -> usage ()
+
     | "-silent" :: rem ->
         Flags.make_silent true; parse rem
 
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 94388f4ac..71b6c9ca0 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -306,6 +306,48 @@ let join_alias (subst1 : substitution) (subst2 : substitution) =
   Umap.mapi (apply_subst subst2) subst1 
 
 
+let update_subst subst1 subst2 =
+ let subst_inv key (mp,_) l =
+    let newmp = 
+      match key with 
+	| MBI msid -> MPbound msid
+	| MSI msid -> MPself msid
+	| MPI mp -> mp
+    in
+   match mp with 
+     | MPbound mbid ->  ((MBI mbid),newmp)::l
+     | MPself msid ->  ((MSI msid),newmp)::l
+     | _ ->   ((MPI mp),newmp)::l
+  in 
+  let subst_mbi = Umap.fold subst_inv subst2 [] in
+  let alias_subst key (mp,_) sub=
+    let newsetkey = 
+      match key with
+	| MPI mp1 -> 
+	    let compute_set_newkey l (k,mp') = 
+	      let mp_from_key = match k with
+		  	| MBI msid -> MPbound msid
+			| MSI msid -> MPself msid
+			| MPI mp -> mp
+	      in
+	      let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in
+		if new_mp1 == mp1 then l else (MPI new_mp1)::l
+	    in
+	    begin
+	      match List.fold_left compute_set_newkey [] subst_mbi with
+		| [] -> None
+		| l -> Some (l)
+	    end
+	| _ -> None
+    in
+      match newsetkey with
+	| None -> sub
+	| Some l -> 
+	    List.fold_left (fun s k -> Umap.add k (mp,None) s)
+	      sub l
+  in
+    Umap.fold alias_subst subst1 empty_subst
+
 
 let subst_substituted s r =
   match !r with
diff --git a/checker/declarations.mli b/checker/declarations.mli
index ceb96d635..fdea3383b 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -208,4 +208,5 @@ val subst_signature_msid :
 val join : substitution -> substitution -> substitution
 val join_alias : substitution -> substitution -> substitution
 val update_subst_alias : substitution -> substitution -> substitution
+val update_subst : substitution -> substitution -> substitution
 val subst_key : substitution -> substitution -> substitution
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 9c1cf8ed3..ecf8d6332 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -182,11 +182,6 @@ let check_definition_sub env cb1 cb2 =
 	Reduction.conv env c1 c2
     | _ -> ())
 
-let is_functor env mb =
-  match type_of_mb env mb with
-    | SEBstruct(msid,str) -> false
-    | _ -> true
-
 let rec check_with env mtb with_decl = 
   match with_decl with
     | With_definition_body _ -> 
@@ -344,13 +339,16 @@ and check_structure_field (s,env) mp lab = function
       (s,Indtypes.check_inductive env kn mib)
   | SFBmodule msb ->
       check_module env msb;
-      ((if is_functor env msb then s else join s msb.mod_alias),
+      let mp1 = MPdot(mp,lab) in
+      let is_fun, sub = Modops.update_subst env msb mp1 in
+      ((if is_fun then s else join s sub),
        Modops.add_module (MPdot(mp,lab)) msb
          (add_module_constraints env msb))
   | SFBalias(mp2,cst) ->
       (try
-        let msb = lookup_module mp2 env in
-        (add_mp (MPdot(mp,lab)) mp2 (join s msb.mod_alias),
+        let mp2' = scrape_alias mp2 env in
+        let msb = lookup_module mp2' env in
+        (join s (add_mp (MPdot(mp,lab)) mp2' msb.mod_alias),
          Option.fold_right add_constraints cst
            (register_alias (MPdot(mp,lab)) mp2 env))
       with Not_found -> failwith "unkown aliased module")
@@ -367,24 +365,27 @@ and check_modexpr env mse = match mse with
   | SEBfunctor (arg_id, mtb, body) ->
       check_module_type env mtb;
       let env' = add_module (MPbound arg_id) (module_body_of_type mtb) env in
-      check_modexpr env' body
+      let sub = check_modexpr env' body in
+      sub
   | SEBapply (f,m,cst) ->
       let sub1 = check_modexpr env f in
       let f'= eval_struct env f in
       let farg_id, farg_b, fbody_b = destr_functor env f' in
-      let mtb = 
-	try
-	  lookup_modtype (path_of_mexpr m) env
-	with
-	  | Not_path -> error_application_to_not_path m
+      let mp =
+	try scrape_alias (path_of_mexpr m) env
+	with Not_path -> error_application_to_not_path m
 	      (* place for nondep_supertype *) in
-      let sub2= check_modexpr env m in
-      let sub = join sub1 sub2 in
-      let sub = join_alias sub (map_mbid farg_id (path_of_mexpr m)) in
-      let sub =
-        update_subst_alias sub (map_mbid farg_id (path_of_mexpr m)) in
+      let mtb = lookup_modtype mp env in
       check_subtypes env mtb farg_b;
-      sub
+      let sub2 = match eval_struct env m with
+	| SEBstruct (msid,sign) -> 
+	    join_alias 
+	      (subst_key (map_msid msid mp) mtb.typ_alias)
+	      (map_msid msid mp)
+	| _ -> mtb.typ_alias in
+      let sub3 = join_alias sub1 (map_mbid farg_id mp) in
+      let sub4 = update_subst sub2 sub3 in
+      join sub3 sub4
   | SEBwith(mte, with_decl) ->
 	let sub1 = check_modexpr env mte in
 	let sub2 = check_with env mte with_decl in
diff --git a/checker/modops.ml b/checker/modops.ml
index fc8636a0b..f79e52c2e 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -339,169 +339,9 @@ and strengthen_sig env msid sign mp = match sign with
     
 let strengthen env mtb mp = strengthen_mtb env mp mtb
 
-
-(*
-
-
-let rec scrape_modtype env = function
-  | MTBident kn ->
-      let mtb =
-        try lookup_modtype kn env
-        with Not_found ->
-          anomalylabstrm "scrape_modtype"
-            (str"scrape_modtype: cannot find "(*++pr_kn kn*)) in
-      scrape_modtype env mtb
-  | mtb -> mtb
-
-
-(* the constraints are not important here *)
-let module_spec_of_body mb = 
-  { msb_modtype = mb.mod_type; 
-    msb_equiv = mb.mod_equiv; 
-    msb_constraints = Constraint.empty}
-
-
-
-let destr_functor = function
-  | MTBfunsig (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
-  | mtb -> error_not_a_functor mtb
-
-let rec check_modpath_equiv env mp1 mp2 = 
-  if mp1=mp2 then () else
-  let mb1 = lookup_module mp1 env in
-    match mb1.mod_equiv with
-      | None ->
-	  let mb2 = lookup_module mp2 env in
-	    (match mb2.mod_equiv with
-	      | None -> error_not_equal mp1 mp2
-	      | Some mp2' -> check_modpath_equiv env mp2' mp1)
-      | Some mp1' -> check_modpath_equiv env mp2 mp1'
-
-
-(* we assume that the substitution of "mp" into "msid" is already done
-(or unnecessary) *)
-let rec add_signature mp sign env = 
-  let add_one env (l,elem) =
-    let kn = make_kn mp empty_dirpath l in
-    let con = make_con mp empty_dirpath l in
-      match elem with
-	| SPBconst cb -> add_constant con cb env
-	| SPBmind mib -> add_mind kn mib env
-	| SPBmodule mb -> 
-	    add_module (MPdot (mp,l)) (module_body_of_spec mb) env 
-	    (* adds components as well *)
-	| SPBmodtype mtb -> add_modtype kn mtb env
-  in
-    List.fold_left add_one env sign
-
-
-and add_module mp mb env = 
-  let env = shallow_add_module mp mb env in
-    match scrape_modtype env mb.mod_type with
-      | MTBident _ -> anomaly "scrape_modtype does not work!"
-      | MTBsig (msid,sign) -> 
-	  add_signature mp (subst_signature_msid msid mp sign) env
-      | MTBfunsig _ -> env
-
-
-let rec constants_of_specification env mp sign =
- let aux (env,res) (l,elem) =
-  match elem with
-   | SPBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
-   | SPBmind _ -> env,res
-   | SPBmodule mb ->
-       let new_env =  add_module (MPdot (mp,l)) (module_body_of_spec mb) env in 
-       new_env,(constants_of_modtype env (MPdot (mp,l))
-		  (module_body_of_spec mb).mod_type) @ res
-   | SPBmodtype mtb -> 
-       (* module type dans un module type. 
-	  Il faut au moins mettre mtb dans l'environnement (avec le bon 
-	  kn pour pouvoir continuer aller deplier les modules utilisant ce 
-	  mtb
-	  ex: 
-	  Module Type T1. 
-	  Module Type T2.
-	     ....
-    	    End T2.
-	  .....
-            Declare Module M : T2.
-         End T2 
-	  si on ne rajoute pas T2 dans l'environement de typage 
-	  on va exploser au moment du Declare Module
-       *)
-       let new_env = add_modtype (make_kn mp empty_dirpath l) mtb env in 
-       new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res
- in
- snd (List.fold_left aux (env,[]) sign)
-
-and constants_of_modtype env mp modtype =
- match scrape_modtype env modtype with
-    MTBident _ -> anomaly "scrape_modtype does not work!"
-  | MTBsig (msid,sign) ->
-     constants_of_specification env mp
-      (subst_signature_msid msid mp sign)
-  | MTBfunsig _ -> []
-
-
-let strengthen_const env mp l cb = 
-  match cb.const_opaque, cb.const_body with
-  | false, Some _ -> cb
-  | true, Some _ 
-  | _, None -> 
-      let const = Const (make_con mp empty_dirpath l) in 
-      let const_subs = Some (from_val const) in
-	{cb with 
-      	   const_body = const_subs;
-	   const_opaque = false(*;
-           const_body_code = Cemitcodes.from_val
-             (compile_constant_body env const_subs false false)*)
-	}
-
-let strengthen_mind env mp l mib = match mib.mind_equiv with
-  | Some _ -> mib
-  | None -> {mib with mind_equiv = Some (make_kn mp empty_dirpath l)}
-    
-let rec strengthen_mtb env mp mtb = match scrape_modtype env mtb with
-  | MTBident _ -> anomaly "scrape_modtype does not work!"
-  | MTBfunsig _ -> mtb
-  | MTBsig (msid,sign) -> MTBsig (msid,strengthen_sig env msid sign mp)
-
-and strengthen_mod env mp msb = 
-  { msb_modtype = strengthen_mtb env mp msb.msb_modtype;
-    msb_equiv = begin match msb.msb_equiv with
-      | Some _ -> msb.msb_equiv
-      | None -> Some mp 
-    end ;
-    msb_constraints = msb.msb_constraints; }
-
-and strengthen_sig env msid sign mp = match sign with
-  | [] -> []
-  | (l,SPBconst cb) :: rest ->
-      let item' = l,SPBconst (strengthen_const env mp l cb) in
-      let rest' = strengthen_sig env msid rest mp in
-	item'::rest'
-  | (l,SPBmind mib) :: rest ->
-      let item' = l,SPBmind (strengthen_mind env mp l mib) in
-      let rest' = strengthen_sig env msid rest mp in
-	item'::rest'
-  | (l,SPBmodule mb) :: rest ->
-      let mp' = MPdot (mp,l) in
-      let item' = l,SPBmodule (strengthen_mod env mp' mb) in
-      let env' = add_module 
-		   (MPdot (MPself msid,l)) 
-		   (module_body_of_spec mb) 
-		   env
-      in
-      let rest' = strengthen_sig env' msid rest mp in
-	item'::rest'
-  | (l,SPBmodtype mty as item) :: rest -> 
-      let env' = add_modtype 
-		   (make_kn (MPself msid) empty_dirpath l) 
-		   mty
-		   env
-      in
-      let rest' = strengthen_sig env' msid rest mp in
-	item::rest'
-
-let strengthen env mtb mp = strengthen_mtb env mp mtb
-*)
+let update_subst env mb mp =
+  match type_of_mb env mb with
+    | SEBstruct(msid,str) -> false, join_alias 
+	(subst_key (map_msid msid mp) mb.mod_alias)
+	(map_msid msid mp)
+    | _ -> true, mb.mod_alias
diff --git a/checker/modops.mli b/checker/modops.mli
index 10b231f44..17b063e2a 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -45,6 +45,8 @@ val check_modpath_equiv : env -> module_path -> module_path -> unit
 
 val strengthen : env -> struct_expr_body -> module_path -> struct_expr_body
 
+val update_subst : env -> module_body -> module_path -> bool * substitution
+
 val error_incompatible_modtypes : 
   module_type_body -> module_type_body -> 'a