checker deals with polymorphic constants and module aliases

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

13 files changed, 280 insertions, 231 deletions

diff --git a/checker/.depend b/checker/.depend
index d9c48a282..dade1591b 100644
--- a/checker/.depend
+++ b/checker/.depend
@@ -1,9 +1,9 @@
-checker.cmo: ../lib/util.cmi univ.cmi type_errors.cmi \
+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 univ.cmx type_errors.cmx \
+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 \
@@ -13,108 +13,104 @@ check.cmo: ../lib/util.cmi ../lib/system.cmi safe_typing.cmi ../lib/pp.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 ../kernel/environ.cmi \
-    declarations.cmi check_stat.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 ../kernel/environ.cmx \
-    declarations.cmx check_stat.cmi 
+    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 esubst.cmi ../kernel/environ.cmi closure.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 esubst.cmx ../kernel/environ.cmx closure.cmi 
-closure.cmi: ../kernel/term.cmi ../lib/pp.cmi ../kernel/names.cmi esubst.cmi \
-    ../kernel/environ.cmi 
-declarations.cmo: ../lib/util.cmi univ.cmi ../kernel/term.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 univ.cmx ../kernel/term.cmx \
+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 univ.cmi ../kernel/term.cmi \
+declarations.cmi: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \
     ../lib/rtree.cmi ../kernel/names.cmi 
-environ.cmo: ../lib/util.cmi univ.cmi ../kernel/term.cmi ../kernel/names.cmi \
-    declarations.cmi 
-environ.cmx: ../lib/util.cmx univ.cmx ../kernel/term.cmx ../kernel/names.cmx \
-    declarations.cmx 
-esubst.cmo: ../lib/util.cmi esubst.cmi 
-esubst.cmx: ../lib/util.cmx esubst.cmi 
-esubst.cmi: ../lib/util.cmi 
-indtypes.cmo: ../lib/util.cmi 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 declarations.cmi \
-    indtypes.cmi 
-indtypes.cmx: ../lib/util.cmx 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 declarations.cmx \
-    indtypes.cmi 
-indtypes.cmi: univ.cmi typeops.cmi ../kernel/term.cmi ../kernel/names.cmi \
-    ../kernel/environ.cmi declarations.cmi 
-inductive.cmo: ../lib/util.cmi 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 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: univ.cmi ../kernel/term.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 \
+    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 \
+    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 
 main.cmo: checker.cmo 
 main.cmx: checker.cmx 
-mod_checking.cmo: ../lib/util.cmi 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 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 univ.cmi ../kernel/term.cmi ../lib/pp.cmi \
-    ../lib/option.cmi ../kernel/names.cmi ../kernel/environ.cmi \
+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 univ.cmx ../kernel/term.cmx ../lib/pp.cmi \
-    ../lib/option.cmx ../kernel/names.cmx ../kernel/environ.cmx \
+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 univ.cmi ../kernel/term.cmi ../kernel/names.cmi \
-    ../kernel/environ.cmi declarations.cmi 
-reduction.cmo: ../lib/util.cmi univ.cmi ../kernel/term.cmi \
-    ../kernel/names.cmi esubst.cmi ../kernel/environ.cmi closure.cmi \
-    reduction.cmi 
-reduction.cmx: ../lib/util.cmx univ.cmx ../kernel/term.cmx \
-    ../kernel/names.cmx esubst.cmx ../kernel/environ.cmx closure.cmx \
-    reduction.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 ../kernel/environ.cmi \
-    declarations.cmi safe_typing.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 ../kernel/environ.cmx \
-    declarations.cmx safe_typing.cmi 
-safe_typing.cmi: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi \
-    declarations.cmi 
-subtyping.cmo: ../lib/util.cmi 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 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: univ.cmi ../kernel/term.cmi ../kernel/environ.cmi \
+    ../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 univ.cmi ../lib/pp.cmi ../lib/option.cmi \
-    ../kernel/names.cmi esubst.cmi 
-term.cmx: ../lib/util.cmx univ.cmx ../lib/pp.cmi ../lib/option.cmx \
-    ../kernel/names.cmx esubst.cmx 
+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 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 univ.cmx type_errors.cmx ../kernel/term.cmx \
-    reduction.cmx ../kernel/names.cmx inductive.cmx ../kernel/environ.cmx \
-    declarations.cmx typeops.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 
-univ.cmo: ../lib/util.cmi ../lib/pp.cmi ../lib/option.cmi ../kernel/names.cmi \
-    univ.cmi 
-univ.cmx: ../lib/util.cmx ../lib/pp.cmi ../lib/option.cmx ../kernel/names.cmx \
-    univ.cmi 
-univ.cmi: ../lib/pp.cmi ../kernel/names.cmi 
diff --git a/checker/check.ml b/checker/check.ml
index 6200a1582..646063519 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -94,16 +94,20 @@ let register_loaded_library m =
   libraries_table := LibraryMap.add m.library_name m !libraries_table
 
 let check_one_lib admit (dir,m) =
+  let file = m.library_filename in
   let md = m.library_compiled in
   let dig = m.library_digest in
+  (* Look up if the library is to be admitted correct. We could
+     also check if it carries a validation certificate (yet to
+     be implemented). *)
   if LibraryMap.mem dir admit then
     (Flags.if_verbose msgnl
       (str "Admitting library: " ++ pr_dirpath dir);
-      Safe_typing.unsafe_import md dig)
+      Safe_typing.unsafe_import file md dig)
   else
     (Flags.if_verbose msgnl
       (str "Checking library: " ++ pr_dirpath dir);
-      Safe_typing.import md dig);
+      Safe_typing.import file md dig);
   Flags.if_verbose msg(fnl());
   register_loaded_library m
 
@@ -288,16 +292,16 @@ let mk_library md f digest = {
   library_digest = digest }
 
 let intern_from_file f =
-  pp (str"[intern "++str f++str" ..."); pp_flush();
+  Flags.if_verbose msg (str"[intern "++str f++str" ...");
   let (md,digest) = 
     try
       let ch = with_magic_number_check raw_intern_library f in
       let (md:library_disk) = System.marshal_in ch in
       let digest = System.marshal_in ch in
       close_in ch;
-      msgnl(str" done]");
+      Flags.if_verbose msgnl(str" done]");
       md,digest
-    with e -> msgnl(str" failed!]"); raise e in
+    with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
   mk_library md f digest
 
 
@@ -343,12 +347,11 @@ let recheck_library ~admit ~check =
   let admit = List.fold_right library_dep al LibraryMap.empty in
   let modl = List.map try_locate_qualified_library check in
   let needed = List.rev (List.fold_right intern_library modl []) in
-  msg(fnl());
-  Flags.if_verbose msgnl (hv 2 (str "Ordered list:" ++ fnl() ++
+  Flags.if_verbose msgnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist
     (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
   List.iter (check_one_lib admit) needed;
-  msgnl(str"Modules were successfully checked"++fnl())
+  Flags.if_verbose msgnl(str"Modules were successfully checked")
 
 open Printf
 
diff --git a/checker/checker.ml b/checker/checker.ml
index e96df366f..832fe0663 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -51,7 +51,7 @@ let get_version_date () =
 
 let print_header () =
   let (ver,rev) = (get_version_date ()) in
-    Printf.printf "Welcome to Coq %s (%s)\n" ver rev;
+    Printf.printf "Welcome to Chicken %s (%s)\n" ver rev;
     flush stdout
 
 (* Adding files to Coq loadpath *)
@@ -194,7 +194,7 @@ let print_usage_channel co command =
 let print_usage = print_usage_channel stderr
 
 let print_usage_coqtop () =
-  print_usage "Usage: checker <options>\n\n"
+  print_usage "Usage: coqchk <options>\n\n"
 
 let usage () =
   print_usage_coqtop ();
@@ -364,11 +364,12 @@ let init() =
   end
 
 let run () =
-  (try 
-    compile_files ()
+  try 
+    compile_files ();
+    flush_all()
   with e ->
-    Pp.ppnl(explain_exn e));
+    (Pp.ppnl(explain_exn e);
     flush_all(); 
-    if not !Flags.debug then exit 0
+    exit 1)
 
-let start () = init(); run()
+let start () = init(); run(); exit 0
diff --git a/checker/declarations.ml b/checker/declarations.ml
index d5c34d92b..94388f4ac 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -39,6 +39,14 @@ type resolver
 type substitution = (module_path * resolver option) Umap.t
 type 'a subst_fun = substitution -> 'a -> 'a
 
+let fold_subst fs fb fp =
+  Umap.fold
+    (fun k (mp,_) acc ->
+      match k with
+          MSI msid -> fs msid mp acc
+        | MBI mbid -> fb mbid mp acc
+        | MPI mp1 -> fp mp1 mp acc)
+
 let empty_subst = Umap.empty
 
 let add_msid msid mp =
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 2145343d3..ceb96d635 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -181,6 +181,12 @@ and module_type_body =
 
 (* Substitutions *)
 
+val fold_subst :
+  (mod_self_id -> module_path -> 'a -> 'a) ->
+  (mod_bound_id -> module_path -> 'a -> 'a) ->
+  (module_path -> module_path -> 'a -> 'a) ->
+  substitution -> 'a -> 'a
+
 type 'a subst_fun = substitution -> 'a -> 'a
 
 val empty_subst : substitution
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 12ae25ca3..8c84fb0fa 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -118,54 +118,6 @@ let small_unit constrsinfos =
   and isunit = is_unit constrsinfos in
   issmall, isunit
 
-(* Computing the levels of polymorphic inductive types
-
-   For each inductive type of a block that is of level u_i, we have
-   the constraints that u_i >= v_i where v_i is the type level of the
-   types of the constructors of this inductive type. Each v_i depends
-   of some of the u_i and of an extra (maybe non variable) universe,
-   say w_i that summarize all the other constraints. Typically, for
-   three inductive types, we could have
-
-   u1,u2,u3,w1 <= u1
-   u1       w2 <= u2
-      u2,u3,w3 <= u3
-
-   From this system of inequations, we shall deduce
-
-   w1,w2,w3 <= u1
-   w1,w2 <= u2
-   w1,w2,w3 <= u3
-*)   
-
-let extract_level (_,_,_,lc,lev) =
-  (* Enforce that the level is not in Prop if more than two constructors *)
-  if Array.length lc >= 2 then sup type0_univ lev else lev
-
-let inductive_levels arities inds =
-  let levels = Array.map pi3 arities in
-  let cstrs_levels = Array.map extract_level inds in
-  (* Take the transitive closure of the system of constructors *)
-  (* level constraints and remove the recursive dependencies *)
-  solve_constraints_system levels cstrs_levels
-
-
-let check_kind env ar u =
-  if snd (dest_prod env ar) = Sort(Type u) then ()
-  else failwith "not the correct sort"
-
-let check_polymorphic_arity env params par =
-  let pl = par.poly_param_levels in
-  let rec check_p env pl params =
-    match pl, params with
-        Some u::pl, (na,None,ty)::params ->
-          check_kind env ty u;
-          check_p (push_rel (na,None,ty) env) pl params
-      | None::pl,d::params -> check_p (push_rel d env) pl params
-      | [], _ -> ()
-      | _ -> failwith "check_poly: not the right number of params" in
-  check_p env pl (List.rev params)
-
 (* check information related to inductive arity *)
 let typecheck_arity env params inds =
   let nparamargs = rel_context_nhyps params in
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 18f190dff..9c1cf8ed3 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -38,7 +38,9 @@ let check_constant_declaration env kn cb =
               let j = infer env' (force_constr bd) in
               conv_leq envty j ty
           | None -> ())
-    | _ -> failwith "polymorphic constants not supported");
+    | PolymorphicArity(ctxt,par) ->
+        let _ = check_ctxt env ctxt in
+        check_polymorphic_arity env ctxt par);
   add_constant kn cb env
 
 (************************************************************************)
@@ -116,7 +118,7 @@ let rec list_fold_map2 f e = function
 	 e'',h1'::t1',h2'::t2'
 
 
-let check_alias s1 s2 =
+let check_alias (s1:substitution) s2 =
   if s1 <> s2 then failwith "Incorrect alias"
 
 let check_definition_sub env cb1 cb2 =
@@ -180,6 +182,11 @@ 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 _ -> 
@@ -328,27 +335,30 @@ and check_module env mb =
 		sub2) in
   check_alias mb.mod_alias sub
 
-and check_structure_field env mp lab = function
+and check_structure_field (s,env) mp lab = function
   | SFBconst cb ->
       let c = make_con mp empty_dirpath lab in
-      check_constant_declaration env c cb
+      (s,check_constant_declaration env c cb)
   | SFBmind mib ->
       let kn = make_kn mp empty_dirpath lab in
-      Indtypes.check_inductive env kn mib
+      (s,Indtypes.check_inductive env kn mib)
   | SFBmodule msb ->
-      let _ = check_module env msb in
-      Modops.add_module (MPdot(mp,lab)) msb
-        (add_module_constraints env msb)
+      check_module env msb;
+      ((if is_functor env msb then s else join s msb.mod_alias),
+       Modops.add_module (MPdot(mp,lab)) msb
+         (add_module_constraints env msb))
   | SFBalias(mp2,cst) ->
-      (* TODO: check mp.lab and mp2 have the same sig *)
       (try
-        let _ = lookup_module mp2 env in
-        register_alias (MPdot(mp,lab)) mp2 env
+        let msb = lookup_module mp2 env in
+        (add_mp (MPdot(mp,lab)) mp2 (join s msb.mod_alias),
+         Option.fold_right add_constraints cst
+           (register_alias (MPdot(mp,lab)) mp2 env))
       with Not_found -> failwith "unkown aliased module")
   | SFBmodtype mty ->
       let kn = MPdot(mp, lab) in
       check_module_type env mty;
-      add_modtype kn mty (add_modtype_constraints env mty)
+      (join s mty.typ_alias,
+       add_modtype kn mty (add_modtype_constraints env mty))
 
 and check_modexpr env mse = match mse with
   | SEBident mp ->
@@ -381,8 +391,7 @@ and check_modexpr env mse = match mse with
 	join sub1 sub2
   | SEBstruct(msid,msb) ->
       let mp = MPself msid in
-      let _ =
+      let (sub,_) =
         List.fold_left (fun env (lab,mb) ->
-          check_structure_field env mp lab mb) env msb in
-      empty_subst
-
+          check_structure_field env mp lab mb) (empty_subst,env) msb in
+      sub
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index c6388499a..4bed9796a 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -225,21 +225,29 @@ type compiled_library =
     (dir_path * Digest.t) list *
     engagement option
  
+(* This function should append a certificate to the .vo file.
+   The digest must be part of the certicate to rule out attackers
+   that could change the .vo file between the time it was read and
+   the time the stamp is written.
+   For the moment, .vo are not signed. *)
+let stamp_library file digest = ()
+
 (* When the module is checked, digests do not need to match, but a
    warning is issued in case of mismatch *)
-let import (dp,mb,depends,engmt as vo) digest = 
-Validate.val_vo (Obj.repr vo);
-prerr_endline "*** vo validated ***";
+let import file (dp,mb,depends,engmt as vo) digest = 
+  Validate.val_vo (Obj.repr vo);
+  Flags.if_verbose msgnl (str "*** vo structure validated ***");
   let env = !genv in
   check_imports msg_warning dp env depends;
   check_engagement env engmt;
   check_module env mb;
+  stamp_library file digest;
   (* We drop proofs once checked *)
 (*  let mb = lighten_module mb in*)
   full_add_module dp mb digest
 
 (* When the module is admitted, digests *must* match *)
-let unsafe_import (dp,mb,depends,engmt) digest = 
+let unsafe_import file (dp,mb,depends,engmt) digest = 
   let env = !genv in
   check_imports (errorlabstrm"unsafe_import") dp env depends;
   check_engagement env engmt;
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 81c48ac2a..12fdbfce8 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -21,5 +21,7 @@ val get_env : unit -> env
 type compiled_library
 
 val set_engagement : Declarations.engagement -> unit
-val import         : compiled_library -> Digest.t -> unit
-val unsafe_import  : compiled_library -> Digest.t -> unit
+val import         :
+  System.physical_path -> compiled_library -> Digest.t -> unit
+val unsafe_import  :
+  System.physical_path -> compiled_library -> Digest.t -> unit
diff --git a/checker/term.ml b/checker/term.ml
index 9e4249396..45568a59a 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -24,7 +24,8 @@ type metavariable = int
 (* This defines the strategy to use for verifiying a Cast *)
 
 (* This defines Cases annotations *)
-type case_style = LetStyle | IfStyle | MatchStyle | RegularStyle
+type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle |
+  RegularStyle
 type case_printing =
   { ind_nargs : int; (* number of real args of the inductive type *)
     style     : case_style }
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 27a3e287d..1af8b2ced 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -436,3 +436,21 @@ let check_named_ctxt env ctxt =
           conv_leq env j1 ty;
           push_named d env)
     ctxt ~init:env
+
+(* Polymorphic arities utils *)
+
+let check_kind env ar u =
+  if snd (dest_prod env ar) = Sort(Type u) then ()
+  else failwith "not the correct sort"
+
+let check_polymorphic_arity env params par =
+  let pl = par.poly_param_levels in
+  let rec check_p env pl params =
+    match pl, params with
+        Some u::pl, (na,None,ty)::params ->
+          check_kind env ty u;
+          check_p (push_rel (na,None,ty) env) pl params
+      | None::pl,d::params -> check_p (push_rel d env) pl params
+      | [], _ -> ()
+      | _ -> failwith "check_poly: not the right number of params" in
+  check_p env pl (List.rev params)
diff --git a/checker/typeops.mli b/checker/typeops.mli
index 6723d82fc..de160a79b 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -21,6 +21,8 @@ val infer      : env -> constr      -> constr
 val infer_type : env -> constr      -> sorts
 val check_ctxt : env -> rel_context -> env
 val check_named_ctxt : env -> named_context -> env
+val check_polymorphic_arity :
+  env -> rel_context -> polymorphic_arity -> unit
 
 val type_of_constant_type : env -> constant_type -> constr
 
diff --git a/checker/validate.ml b/checker/validate.ml
index 2eb1ec0cf..86e51b7b9 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -1,5 +1,17 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
-let rec pr_obj o =
+(* $Id: term.ml 10098 2007-08-27 11:41:08Z herbelin $ *)
+
+(* This module defines validation functions to ensure an imported
+   value (using input_value) has the correct structure. *)
+
+let rec pr_obj_rec o =
   if Obj.is_int o then
     Format.print_string ("INT:"^string_of_int(Obj.magic o))
   else if Obj.is_block o then
@@ -14,86 +26,112 @@ let rec pr_obj o =
       Format.print_string ("#"^string_of_int t^"(");
       Format.open_hvbox 0;
       for i = 0 to n-1 do
-        pr_obj (Obj.field o i);
+        pr_obj_rec (Obj.field o i);
         if i<>n-1 then (Format.print_string ","; Format.print_cut())
       done;
       Format.close_box();
       Format.print_string ")")
   else Format.print_string "?"
 
-let pr_obj o = pr_obj o; Format.print_newline()
-
+let pr_obj o = pr_obj_rec o; Format.print_newline()
 
+(**************************************************************************)
+(* Low-level validators *)
 
+(* data not validated *)
 let no_val (o:Obj.t) = ()
 
+(* Check that object o is a block with tag t *)
 let val_tag t o =
   if Obj.is_block o && Obj.tag o = t then ()
   else failwith ("tag "^string_of_int t)
 
-let val_tuple s v o =
-  let n = Array.length v in
+let val_obj s o =
   if Obj.is_block o then
-    if Obj.size o = n then
-      Array.iteri (fun i f -> f (Obj.field o i)) v
-    else
-      (pr_obj o;
-       failwith
-         ("tuple:" ^s^" size found:"^string_of_int (Obj.size o)))
-  else failwith ("tuple:" ^s)
+    (if Obj.tag o > Obj.no_scan_tag then
+      failwith (s^". Not a normal tag"))
+  else failwith (s^". Not a block")
 
+(* Check that an object is a tuple (or a record). v is an array of
+   validation functions for each field. Its size corresponds to the
+   expected size of the object. *)
+let val_tuple s v o =
+  let n = Array.length v in
+  val_obj ("tuple: "^s) o;
+  if Obj.size o = n then
+    Array.iteri (fun i f -> f (Obj.field o i)) v
+  else
+    (pr_obj o;
+     failwith
+       ("tuple:" ^s^" size found:"^string_of_int (Obj.size o)))
+
+(* Check that the object is either a constant constructor of tag < cc,
+   or a constructed variant. each element of vv is an array of
+   validation functions to be applied to the constructor arguments.
+   The size of vv corresponds to the number of non-constant
+   constructors, and the size of vv.(i) is the expected arity of the
+   i-th non-constant constructor. *)
 let val_sum s cc vv o =
   if Obj.is_block o then
+    (val_obj ("sum: "^s) o;
     let n = Array.length vv in
     let i = Obj.tag o in
     if i < n then val_tuple (s^"("^string_of_int i^")") vv.(i) o
-    else failwith ("bad tag in sum: "^string_of_int i)
+    else failwith ("bad tag in sum ("^s^"): "^string_of_int i))
   else if Obj.is_int o then
     let (n:int) = Obj.magic o in
-    (if n<0 || n>=cc then failwith "bad constant constructor")
-  else failwith "not a sum"
+    (if n<0 || n>=cc then failwith ("bad constant constructor ("^s^")"))
+  else failwith ("not a sum ("^s^")")
 
+let val_enum s n = val_sum s n [||]
+
+(* Recursive types: avoid looping by eta-expansion *)
+let rec val_rec_sum s cc f o =
+  val_sum s cc (f (val_rec_sum s cc f)) o
+
+(**************************************************************************)
+(* Builtin types *)
+
+(* Check the o is an array of values satisfying f. *)
 let val_array f o =
-  if Obj.is_block o then
-    for i = 0 to Obj.size o - 1 do
-      (f (Obj.field o i):unit)
-    done
-  else failwith "not array"
-(*
-let val_tuple s v o =
-  prerr_endline ("TUPLE "^s);
-  val_tuple s v o;
-  prerr_endline ("END "^s)
-let val_sum s cc vv o =
-  prerr_endline ("SUM "^s);
-  val_sum s cc vv o;
-  prerr_endline ("END "^s)
-let val_array f o =
-  prerr_endline "ARRAY";
-  val_array f o;
-  prerr_endline "END ARRAY"
-*)
-let val_int o = if not (Obj.is_int o) then failwith "not int"
-(*; prerr_endline "INT"
-*)
+  val_obj "array" o;
+  for i = 0 to Obj.size o - 1 do
+    (f (Obj.field o i):unit)
+  done
+
+(* Integer validator *)
+let val_int o =
+  if not (Obj.is_int o) then failwith "expected an int"
+
+(* String validator *)
 let val_str s = val_tag Obj.string_tag s
-(*; prerr_endline ("STR "^Obj.magic s)*)
 
-let val_bool o = val_sum "bool" 2 [||] o
+(* Booleans *)
+let val_bool = val_enum "bool" 2
 
+(* Option type *)
 let val_opt f = val_sum "option" 1 [|[|f|]|]
 
-let rec val_list f o =
-  val_sum "list" 1 [|[|f;val_list f|]|] o
+(* Lists *)
+let val_list f =
+  val_rec_sum "list" 1 (fun vlist -> [|[|f;vlist|]|])
 
+(* Reference *)
 let val_ref f = val_tuple "ref" [|f|]
 
-let rec val_set f o =
-  val_sum "set" 1 [|[|val_set f;f;val_set f;val_int|]|] o
-let rec val_map fk fv o =
-  val_sum "map" 1 [|[|val_map fk fv;fk;fv;val_map fk fv;val_int|]|] o
+(**************************************************************************)
+(* Standard library types *)
+
+(* Sets *)
+let val_set f =
+  val_rec_sum "set" 1 (fun vset -> [|[|vset;f;vset;val_int|]|])
+
+(* Maps *)
+let rec val_map fk fv =
+  val_rec_sum "map" 1 (fun vmap -> [|[|vmap;fk;fv;vmap;val_int|]|])
 
-(* Coq *)
+(**************************************************************************)
+(* Coq types *)
 
 let val_id = val_str
 
@@ -103,27 +141,31 @@ let val_name = val_sum "name" 1 [|[|val_id|]|]
 
 let val_uid = val_tuple "uid" [|val_int;val_str;val_dp|]
 
-let rec val_mp o =
-  val_sum "mp" 0 [|[|val_dp|];[|val_uid|];[|val_uid|];[|val_mp;val_id|]|] o
+let val_mp =
+  val_rec_sum "mp" 0
+    (fun vmp -> [|[|val_dp|];[|val_uid|];[|val_uid|];[|vmp;val_id|]|])
 
 let val_kn = val_tuple "kn" [|val_mp;val_dp;val_id|]
 
 let val_ind = val_tuple "ind"[|val_kn;val_int|]
 let val_cstr = val_tuple "cstr"[|val_ind;val_int|]
 
-let val_ci = no_val
+let val_ci =
+  let val_cstyle = val_enum "case_style" 5 in
+  let val_cprint = val_tuple "case_printing" [|val_int;val_cstyle|] in
+  val_tuple "case_info" [|val_ind;val_int;val_array val_int;val_cprint|]
 
-let val_cast = no_val
 
 let val_level = val_sum "level" 1 [|[|val_dp;val_int|]|]
 let val_univ = val_sum "univ" 0
   [|[|val_level|];[|val_list val_level;val_list val_level|]|]
 
 let val_cstrs =
-  val_set (val_tuple"univ_cstr"[|val_level;val_sum "order" 3[||];val_level|])
+  val_set (val_tuple"univ_cstr"[|val_level;val_enum "order" 3;val_level|])
 
-let val_sort = val_sum "sort" 0 [|[|val_sum "cnt" 2 [||]|];[|val_univ|]|]
-let val_sortfam = val_sum "sort_family" 3 [||]
+let val_cast = val_enum "cast_kind" 2
+let val_sort = val_sum "sort" 0 [|[|val_enum "cnt" 2|];[|val_univ|]|]
+let val_sortfam = val_enum "sort_family" 3
 
 let val_evar f = val_tuple "evar" [|val_int;val_array f|]
 
@@ -134,7 +176,7 @@ let val_fix f =
 let val_cofix f = val_tuple"cofix"[|val_int;val_prec f|]
 
 
-let rec val_constr o = val_sum "constr" 0 [|
+let val_constr = val_rec_sum "constr" 0 (fun val_constr -> [|
   [|val_int|]; (* Rel *)
   [|val_id|]; (* Var *)
   [|val_int|]; (* Meta *)
@@ -151,7 +193,7 @@ let rec val_constr o = val_sum "constr" 0 [|
   [|val_ci;val_constr;val_constr;val_array val_constr|]; (* Case *)
   [|val_fix val_constr|]; (* Fix *)
   [|val_cofix val_constr|] (* CoFix *)
-|] o
+|])
 
 
 let val_ndecl = val_tuple"ndecl"[|val_id;val_opt val_constr;val_constr|]
@@ -161,7 +203,7 @@ let val_rctxt = val_list val_rdecl
 
 let val_arity = val_tuple"arity"[|val_rctxt;val_constr|]
 
-let val_eng = val_sum "eng" 1 [||]
+let val_eng = val_enum "eng" 1
 
 let val_pol_arity = val_tuple"pol_arity"[|val_list(val_opt val_univ);val_univ|]
 let val_cst_type =
@@ -185,9 +227,10 @@ let val_cb = val_tuple "cb"
 
 let val_recarg = val_sum "recarg" 1 [|[|val_int|];[|val_ind|]|]
 
-let rec val_wfp o = val_sum "wf_paths" 0
-  [|[|val_int;val_int|];[|val_recarg;val_array val_wfp|];
-    [|val_int;val_array val_wfp|]|] o
+let val_wfp = val_rec_sum "wf_paths" 0
+  (fun val_wfp -> 
+    [|[|val_int;val_int|];[|val_recarg;val_array val_wfp|];
+      [|val_int;val_array val_wfp|]|])
 
 let val_mono_ind_arity = val_tuple"mono_ind_arity"[|val_constr;val_sort|]
 let val_ind_arity = val_sum "ind_arity" 0