modules

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

13 files changed, 164 insertions, 121 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 11923a3e24..8766467fce 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -40,7 +40,9 @@ let make_strength_2 () =
 
 (* Variables. *)
 
-type variable_declaration = constr * strength * bool
+type sticky = bool
+
+type variable_declaration = constr * strength * sticky
 
 let vartab = ref (Spmap.empty : (identifier * variable_declaration) Spmap.t)
 
@@ -49,10 +51,10 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.unfreeze_function = (fun ft -> vartab := ft);
 	    Summary.init_function = (fun () -> vartab := Spmap.empty) }
 
-let cache_variable (sp,(id,(ty,_,_) as vd)) = 
+let cache_variable (sp,(id,(ty,_,_) as vd,imps)) = 
   Global.push_var (id,ty);
   Nametab.push id sp;
-  declare_var_implicits id;
+  if imps then declare_var_implicits id;
   vartab := Spmap.add sp vd !vartab
 
 let load_variable _ = anomaly "we shouldn't load a variable"
@@ -70,34 +72,36 @@ let (in_variable, out_variable) =
     specification_function = specification_variable } in
   declare_object ("VARIABLE", od)
 
-let declare_variable id ((ty,_,_) as obj) =
-  let _ = add_leaf id CCI (in_variable (id,obj)) in
+let declare_variable id obj =
+  let _ = add_leaf id CCI (in_variable ((id,obj),is_implicit_args())) in
   ()
 
 (* Parameters. *)
 
-let cache_parameter (sp,c) =
+let cache_parameter (sp,(c,imps)) =
   Global.add_parameter sp c;
   Nametab.push (basename sp) sp;
-  declare_constant_implicits sp
+  if imps then declare_constant_implicits sp
+
+let load_parameter (sp,(_,imps)) =
+  if imps then declare_constant_implicits sp
 
 let open_parameter (sp,_) =
-  Nametab.push (basename sp) sp;
-  declare_constant_implicits sp
+  Nametab.push (basename sp) sp
 
 let specification_parameter obj = obj
 
 let (in_parameter, out_parameter) =
   let od = {
     cache_function = cache_parameter;
-    load_function = (fun _ -> ());
+    load_function = load_parameter;
     open_function = open_parameter;
     specification_function = specification_parameter } 
   in
   declare_object ("PARAMETER", od)
 
 let declare_parameter id c =
-  let _ = add_leaf id CCI (in_parameter c) in ()
+  let _ = add_leaf id CCI (in_parameter (c,is_implicit_args())) in ()
 
 (* Constants. *)
 
@@ -110,14 +114,14 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.unfreeze_function = (fun ft -> csttab := ft);
 	    Summary.init_function = (fun () -> csttab := Spmap.empty) }
 
-let cache_constant (sp,((ce,_) as cd)) =
+let cache_constant (sp,((ce,_) as cd,imps)) =
   Global.add_constant sp ce;
   Nametab.push (basename sp) sp;
-  declare_constant_implicits sp;
+  if imps then declare_constant_implicits sp;
   csttab := Spmap.add sp cd !csttab
 
-let load_constant (sp,((ce,_) as cd)) =
-  declare_constant_implicits sp;
+let load_constant (sp,((ce,_) as cd,imps)) =
+  if imps then declare_constant_implicits sp;
   csttab := Spmap.add sp cd !csttab
 
 let open_constant (sp,_) =
@@ -135,7 +139,7 @@ let (in_constant, out_constant) =
   declare_object ("CONSTANT", od)
 
 let declare_constant id cd =
-  let _ = add_leaf id CCI (in_constant cd) in ()
+  let _ = add_leaf id CCI (in_constant (cd,is_implicit_args())) in ()
 
  
 (* Inductives. *)
@@ -147,15 +151,15 @@ let push_inductive_names sp mie =
        List.iter (fun x -> Nametab.push x sp) cnames)
     mie.mind_entry_inds
 
-let cache_inductive (sp,mie) =
+let cache_inductive (sp,(mie,imps)) =
   Global.add_mind sp mie;
   push_inductive_names sp mie;
-  declare_inductive_implicits sp
+  if imps then declare_inductive_implicits sp
 
-let load_inductive (sp,_) =
-  declare_inductive_implicits sp
+let load_inductive (sp,(_,imps)) =
+  if imps then declare_inductive_implicits sp
 
-let open_inductive (sp,mie) =
+let open_inductive (sp,(mie,_)) =
   push_inductive_names sp mie
 
 let specification_inductive obj = obj
@@ -163,7 +167,7 @@ let specification_inductive obj = obj
 let (in_inductive, out_inductive) =
   let od = {
     cache_function = cache_inductive;
-    load_function = (fun _ -> ());
+    load_function = load_inductive;
     open_function = open_inductive;
     specification_function = specification_inductive } 
   in
@@ -174,7 +178,7 @@ let declare_mind mie =
     | (id,_,_,_)::_ -> id
     | [] -> anomaly "cannot declare an empty list of inductives"
   in
-  let sp = add_leaf id CCI (in_inductive mie) in
+  let sp = add_leaf id CCI (in_inductive (mie,is_implicit_args())) in
   sp
 
 
@@ -297,7 +301,7 @@ let declare_eliminations sp i =
     declare_constant (id_of_string na)
       ({ const_entry_body = Cooked c; const_entry_type = None }, 
        NeverDischarge);
-    pPNL [< 'sTR na; 'sTR " is defined" >]
+    if Options.is_verbose() then pPNL [< 'sTR na; 'sTR " is defined" >]
   in
   let env = Global.env () in
   let sigma = Evd.empty in
diff --git a/library/declare.mli b/library/declare.mli
index 15722dbc0a..c4644b4654 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -20,7 +20,9 @@ type strength =
   | DischargeAt of section_path 
   | NeverDischarge
 
-type variable_declaration = constr * strength * bool
+type sticky = bool
+
+type variable_declaration = constr * strength * sticky
 val declare_variable : identifier -> variable_declaration -> unit
 
 type constant_declaration = constant_entry * strength
@@ -43,7 +45,8 @@ val is_constant : section_path -> bool
 val constant_strength : section_path -> strength
 
 val is_variable : identifier -> bool
-val out_variable : section_path -> identifier * typed_type * strength * bool
+val out_variable : 
+  section_path -> identifier * typed_type * strength * sticky
 val variable_strength : identifier -> strength
 
 
diff --git a/library/impargs.ml b/library/impargs.ml
index 8198732826..1a9b741c42 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -31,11 +31,8 @@ let implicitely f x =
   end
 
 let auto_implicits ty =
-  if !implicit_args then
-    let genv = Global.env() in
-    Impl_auto (poly_args genv Evd.empty ty)
-  else
-    No_impl
+  let genv = Global.env() in
+  Impl_auto (poly_args genv Evd.empty ty)
 
 let list_of_implicits = function 
   | Impl_auto l -> l
@@ -55,7 +52,10 @@ let declare_constant_manual_implicits sp imps =
   constants_table := Spmap.add sp (Impl_manual imps) !constants_table
 
 let constant_implicits sp =
-  Spmap.find sp !constants_table
+  try Spmap.find sp !constants_table with Not_found -> No_impl
+
+let constant_implicits_list sp =
+  list_of_implicits (constant_implicits sp)
 
 (* Inductives and constructors. Their implicit arguments are stored
    in an array, indexed by the inductive number, of pairs $(i,v)$ where
@@ -75,12 +75,16 @@ let declare_inductive_implicits sp =
   inductives_table := Spmap.add sp imps !inductives_table
     
 let inductive_implicits (sp,i) =
-  let imps = Spmap.find sp !inductives_table in
-  fst imps.(i)
+  try
+    let imps = Spmap.find sp !inductives_table in fst imps.(i)
+  with Not_found -> 
+    No_impl
 
 let constructor_implicits ((sp,i),j) =
-  let imps = Spmap.find sp !inductives_table in
-  (snd imps.(i)).(pred j)
+  try
+    let imps = Spmap.find sp !inductives_table in (snd imps.(i)).(pred j)
+  with Not_found -> 
+    No_impl
 
 let constructor_implicits_list constr_sp = 
   list_of_implicits (constructor_implicits constr_sp)
@@ -88,9 +92,6 @@ let constructor_implicits_list constr_sp =
 let inductive_implicits_list ind_sp =
   list_of_implicits (inductive_implicits ind_sp)
 
-let constant_implicits_list sp =
-  list_of_implicits (constant_implicits sp)
-
 (* Variables. *)
 
 let var_table = ref Idmap.empty
@@ -101,11 +102,12 @@ let declare_var_implicits id =
   var_table := Idmap.add id imps !var_table
 
 let implicits_of_var _ id =
-  list_of_implicits (Idmap.find id !var_table)
+  list_of_implicits (try Idmap.find id !var_table with Not_found -> No_impl)
 
 (* Registration as global tables and roolback. *)
 
-type frozen_t = implicits Spmap.t 
+type frozen_t = bool
+              * implicits Spmap.t 
               * (implicits * implicits array) array Spmap.t 
               * implicits Idmap.t
 
@@ -115,9 +117,10 @@ let init () =
   var_table := Idmap.empty
 
 let freeze () =
-  !constants_table, !inductives_table, !var_table
+  (!implicit_args,!constants_table, !inductives_table, !var_table)
 
-let unfreeze (ct,it,vt) =
+let unfreeze (imps,ct,it,vt) =
+  implicit_args := imps;
   constants_table := ct;
   inductives_table := it;
   var_table := vt
diff --git a/library/lib.ml b/library/lib.ml
index f79c22c58c..a6686168da 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -8,12 +8,13 @@ open Summary
 
 type node = 
   | Leaf of obj
+  | Module of string
   | OpenedSection of string * Summary.frozen
   | FrozenState of Summary.frozen
 
-and library_segment = (section_path * node) list
+and library_entry = section_path * node
 
-type library_entry = section_path * node
+and library_segment = library_entry list
 
 
 (* We keep trace of operations in the stack [lib_stk]. 
@@ -109,13 +110,15 @@ let check_for_module () =
   let is_decl = function (_,FrozenState _) -> false | _ -> true in
   try
     let _ = find_entry_p is_decl in
-    error "a module can not be opened after some declarations"
+    error "a module can not be started after some declarations"
   with Not_found -> ()
 
-let open_module s =
-  if !module_name <> None then error "a module is already opened";
-  check_for_module ();
-  module_name := Some s
+let start_module s =
+  if !module_name <> None then error "a module is already started";
+  if !path_prefix <> [] then error "some sections are already opened";
+  module_name := Some s;
+  let _ = add_anonymous_entry (Module s) in
+  path_prefix := [s]
 
 let is_opened_section = function (_,OpenedSection _) -> true | _ -> false
 
@@ -135,15 +138,16 @@ let close_section s =
 
 (* The following function exports the whole library segment, that will be 
    saved as a module. Objects are presented in chronological order, and
-   closed sections and frozen states are removed. *)
+   frozen states are removed. *)
 
 let export_module () =
   if !module_name = None then error "no module declared";
   let rec export acc = function
-    | [] -> acc
+    | (_,Module _) :: _ -> acc
     | (_,Leaf _) as node :: stk -> export (node::acc) stk
     | (_,OpenedSection _) :: _ -> error "there are still opened sections"
     | (_,FrozenState _) :: stk -> export acc stk
+    | _ -> assert false
   in
   export [] !lib_stk
 
diff --git a/library/lib.mli b/library/lib.mli
index 2fe172f9f6..36b49bbeb2 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -13,12 +13,13 @@ open Summary
 
 type node = 
   | Leaf of obj
+  | Module of string
   | OpenedSection of string * Summary.frozen
   | FrozenState of Summary.frozen
 
-and library_segment = (section_path * node) list
+and library_entry = section_path * node
 
-type library_entry = section_path * node
+and library_segment = library_entry list
 
 
 (*s Adding operations (which calls the [cache] method, and getting the
@@ -39,7 +40,7 @@ val make_path : identifier -> path_kind -> section_path
 val cwd : unit -> string list
 val is_section_p : section_path -> bool
 
-val open_module : string -> unit
+val start_module : string -> unit
 val export_module : unit -> library_segment
 
 
diff --git a/library/library.ml b/library/library.ml
index cbd4789532..913f396d94 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -63,7 +63,7 @@ let segment_iter f =
   let rec apply = function
     | sp,Leaf obj -> f (sp,obj)
     | _,OpenedSection _ -> assert false
-    | _,FrozenState _ -> ()
+    | _,(FrozenState _ | Module _) -> ()
   and iter seg =
     List.iter apply seg
   in
@@ -91,8 +91,8 @@ let load_objects decls =
 
 let rec load_module_from doexp s f =
   let (fname,ch) = raw_intern_module f in
-  let md = input_value ch in
-  let digest = input_value ch in
+  let md = System.marshal_in ch in
+  let digest = System.marshal_in ch in
   close_in ch;
   let m = { module_name = md.md_name;
 	    module_compiled_env = md.md_compiled_env;
@@ -151,11 +151,11 @@ let save_module_to s f =
     md_compiled_env = Global.export s;
     md_declarations = seg;
     md_deps = current_imports () } in
-  let (_,ch) = raw_extern_module f in
-  output_value ch md;
+  let (f',ch) = raw_extern_module f in
+  System.marshal_out ch md;
   flush ch;
-  let di = Digest.file f in
-  output_value ch di;
+  let di = Digest.file f' in
+  System.marshal_out ch di;
   close_out ch
 
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 776864d705..6a0a2e2a98 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -3,6 +3,7 @@
 
 open Pp
 open Util
+open Options
 open Generic
 open Term
 open Constant
@@ -40,7 +41,8 @@ let constant_entry_of_com com =
 
 let definition_body ident n com = 
   let ce = constant_entry_of_com com in
-  declare_constant ident (ce,n)
+  declare_constant ident (ce,n);
+  if is_verbose() then message ((string_of_id ident) ^ " is defined")
 
 let red_constant_entry ce = function
   | None -> ce
@@ -57,11 +59,14 @@ let red_constant_entry ce = function
 let definition_body_red ident n com red_option = 
   let ce = constant_entry_of_com com in
   let ce' = red_constant_entry ce red_option in
-  declare_constant ident (ce',n)
+  declare_constant ident (ce',n);
+  if is_verbose() then message ((string_of_id ident) ^ " is defined")
 
 let syntax_definition ident com =
   let c = raw_constr_of_com Evd.empty (Global.context()) com in 
-  Syntax_def.declare_syntactic_definition ident c
+  Syntax_def.declare_syntactic_definition ident c;
+  if is_verbose() then 
+    message ((string_of_id ident) ^ " is now a syntax macro")
 
 (***TODO
 let abstraction_definition ident arity com =
@@ -158,7 +163,7 @@ let build_mutual lparams lnamearconstrs finite =
     in
     States.unfreeze fs;
     let sp = declare_mind mie in
-    pPNL(minductive_message lrecnames);
+    if is_verbose() then pPNL(minductive_message lrecnames);
     for i = 0 to List.length mispecvec - 1 do
       declare_eliminations sp i
     done
@@ -248,7 +253,7 @@ let build_recursive lnameargsardef =
     in 
     (* declare the recursive definitions *)
     declare 0 lnamerec; 
-    pPNL(recursive_message lnamerec)
+    if is_verbose() then pPNL(recursive_message lnamerec)
   end;
   (* The others are declared as normal definitions *)
   let var_subst id = (id,make_substituend (global_reference CCI id)) in
@@ -313,7 +318,7 @@ let build_corecursive lnameardef =
       | _        -> () 
     in 
     declare 0 lnamerec; 
-    pPNL(corecursive_message lnamerec)
+    if is_verbose() then pPNL(corecursive_message lnamerec)
   end;
   let var_subst id =
     (id,make_substituend (global_reference CCI id)) in
@@ -351,4 +356,6 @@ let build_scheme lnamedepindsort =
         declare (i+1) lf
     | _        -> ()
   in 
-  declare 0 lrecnames; pPNL(recursive_message lrecnames)
+  declare 0 lrecnames; 
+  if is_verbose() then pPNL(recursive_message lrecnames)
+
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 282039d986..01cfeb4e24 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -55,12 +55,10 @@ let require () =
     (List.rev !require_list)
 
 
-(*
- * Parsing of the command line.
+(* Parsing of the command line.
  *
- * We no longer use Arg.parse, in order to use Usage.print_usage to be coherent
- * with launch/coqtop and launch/coqc.
- *)
+ * We no longer use Arg.parse, in order to use share Usage.print_usage 
+ * between coqtop and coqc. *)
 
 let usage () =
   if !batch_mode then
@@ -70,62 +68,75 @@ let usage () =
   flush stderr ;
   exit 1
 
+let version () =
+  Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
+    Coq_config.version Coq_config.date;
+  Printf.printf "compiled on %s\n" Coq_config.compile_date;
+  exit 0
 
 let parse_args () =
   let rec parse = function
     | [] -> ()
 
-    | ("-I"|"-include") :: d :: rem -> push_include d ; parse rem
+    | ("-I"|"-include") :: d :: rem -> push_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
 
-    | ("-R") :: d :: rem -> rec_include d ; parse rem
-    | ("-R") :: []       -> usage ()
+    | "-R" :: d :: rem -> rec_include d; parse rem
+    | "-R" :: []       -> usage ()
 
-    | "-q" :: rem -> no_load_rc () ; parse rem
+    | "-q" :: rem -> no_load_rc (); parse rem
 
-    | "-batch" :: rem -> set_batch_mode () ; parse rem
+    | "-batch" :: rem -> set_batch_mode (); parse rem
 	     
-    | "-outputstate" :: s :: rem -> set_outputstate s ; parse rem
+    | "-outputstate" :: s :: rem -> set_outputstate s; parse rem
     | "-outputstate" :: []       -> usage ()
 
-    | "-nois" :: rem -> set_inputstate "" ; parse rem
+    | "-nois" :: rem -> set_inputstate ""; parse rem
 	     
-    | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s ; parse rem
+    | ("-inputstate"|"-is") :: s :: rem -> set_inputstate s; parse rem
     | ("-inputstate"|"-is") :: []       -> usage ()
 
-    | "-load-ml-object" :: f :: rem -> Mltop.dir_ml_load f ; parse rem
+    | "-load-ml-object" :: f :: rem -> Mltop.dir_ml_load f; parse rem
     | "-load-ml-object" :: []       -> usage ()
 
-    | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f ; parse rem
+    | "-load-ml-source" :: f :: rem -> Mltop.dir_ml_use f; parse rem
     | "-load-ml-source" :: []       -> usage ()
 
-    | "-load-vernac-source" :: f :: rem -> add_load_vernacular f ; parse rem
+    | "-load-vernac-source" :: f :: rem -> add_load_vernacular f; parse rem
     | "-load-vernac-source" :: []       -> usage ()
 
-    | "-load-vernac-object" :: f :: rem -> add_vernac_obj f ; parse rem
+    | "-load-vernac-object" :: f :: rem -> add_vernac_obj f; parse rem
     | "-load-vernac-object" :: []       -> usage ()
 
-    | "-require" :: f :: rem -> add_require f ; parse rem
+    | "-require" :: f :: rem -> add_require f; parse rem
     | "-require" :: []       -> usage ()
 
-    | "-unsafe" :: f :: rem -> add_unsafe f ; parse rem
+    | "-unsafe" :: f :: rem -> add_unsafe f; parse rem
     | "-unsafe" :: []       -> usage ()
 
-    | "-debug" :: rem -> set_debug () ; parse rem
+    | "-debug" :: rem -> set_debug (); parse rem
 
-    | "-emacs" :: rem -> Printer.print_emacs := true ; parse rem
+    | "-emacs" :: rem -> Printer.print_emacs := true; parse rem
+	  
+    | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
 
-    | "-init-file" :: f :: rem -> set_rcfile f ; parse rem
+    | ("-quiet"|"-silent") :: rem -> Options.make_silent true; parse rem
+
+    | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
+
+    | ("-v"|"--version") :: _ -> version ()
+
+    | "-init-file" :: f :: rem -> set_rcfile f; parse rem
     | "-init-file" :: []       -> usage ()
 
-    | "-user" :: u :: rem -> set_rcuser u ; parse rem
+    | "-user" :: u :: rem -> set_rcuser u; parse rem
     | "-user" :: []       -> usage ()
 
-    | "-notactics" :: rem -> remove_top_ml () ; parse rem
+    | "-notactics" :: rem -> remove_top_ml (); parse rem
 
-    | "-just-parsing" :: rem -> Vernac.just_parsing := true ; parse rem
+    | "-just-parsing" :: rem -> Vernac.just_parsing := true; parse rem
 
-    | s :: _ -> prerr_endline ("Don't know what to do with " ^ s) ; usage ()
+    | s :: _ -> prerr_endline ("Don't know what to do with " ^ s); usage ()
 
   in
   try
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index f0a97c2180..15f52e412b 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -182,11 +182,11 @@ let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
 (* Discharge of the various objects of the environment. *)
 
 let constant_message id =
-  if Options.verbose() then 
+  if Options.is_verbose() then 
     pPNL [< print_id id; 'sTR " is discharged." >]
 
 let inductive_message inds =
-  if Options.verbose() then 
+  if Options.is_verbose() then 
     pPNL (hOV 0 
 	    (match inds with
 	       | [] -> assert false
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index af8b7c5cbf..ba1f36cd7c 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -48,9 +48,9 @@ let rec explain_exn_default = function
 
   | Sys.Break -> hOV 0 [< 'fNL; 'sTR"User Interrupt." >]
 
-  | TypeError(k,ctx,te) -> Himsg.explain_type_error k ctx te
+  | TypeError(k,ctx,te) -> hOV 0 (Himsg.explain_type_error k ctx te)
 
-  | InductiveError e -> Himsg.explain_inductive_error e
+  | InductiveError e -> hOV 0 (Himsg.explain_inductive_error e)
 
   | Stdpp.Exc_located (loc,exc) ->
       hOV 0 [< if loc = Ast.dummy_loc then [<>]
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index d2a2400754..3135d53fc4 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -263,7 +263,7 @@ let _ = vinterp_add "PrintMLPath"
 let print_ml_modules () =
   let l = get_loaded_modules () in
   pP [< 'sTR"Loaded ML Modules : " ;
-        hOV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >]
+        hOV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l); 'fNL >]
 
 let _ = vinterp_add "PrintMLModules"
 	  (function 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 2c230365df..a87e61bc53 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -9,7 +9,7 @@ let print_usage_channel co command =
   output_string co
 "  -I dir                 add directory dir in the include path
   -include dir           (idem)
-  -R dir                 add recursively dir
+  -R dir                 add dir recursively
   -src                   add source directories in the include path
 
   -inputstate f          read state from file f.coq
@@ -33,8 +33,8 @@ let print_usage_channel co command =
   -v                     print Coq version and exit
 
   -q                     skip loading of rcfile
-  -init-file f           give the rcfile f
-  -user u                give the user u
+  -init-file f           set the rcfile to f
+  -user u                use the rcfile of user u
   -batch                 batch mode (exits just after arguments parsing)
   -emacs                 tells Coq it is executed under Emacs
 "
@@ -46,7 +46,7 @@ let print_usage = print_usage_channel stderr
 let print_usage_coqtop () =
   print_usage "Usage: coqtop <options>\n";
   output_string stderr
-"  -searchisos            run Coq_SearchIsos\n";;
+"  -searchisos            run Coq_SearchIsos\n"
 
 let print_usage_coqc () =
   print_usage "Usage: coqc [-i] [-t] <options> file...\n
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 93a3303165..a50dcfdf50 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -269,10 +269,19 @@ let _ =
   add "BeginModule"
     (function 
        | [VARG_IDENTIFIER id] ->
-	   fun () -> Library.open_module (string_of_id id)
+	   fun () -> Lib.start_module (string_of_id id)
        | _ -> bad_vernac_args "BeginModule")
 
 let _ =
+  add "WriteModule"
+    (function 
+       | [VARG_IDENTIFIER id] ->
+	   fun () -> let m = string_of_id id in Library.save_module_to m m
+       | [VARG_IDENTIFIER id; VARG_STRING f] ->
+	   fun () -> Library.save_module_to (string_of_id id) f
+       | _ -> bad_vernac_args "WriteModule")
+
+let _ =
   add "ReadModule"
     (function 
        | [VARG_IDENTIFIER id] ->
@@ -281,19 +290,27 @@ let _ =
        | _ -> bad_vernac_args "ReadModule")
 
 let _ =
+  add "ImportModule"
+    (function 
+       | [VARG_IDENTIFIER id] ->
+	   fun () -> 
+	     without_mes_ambig Library.open_module (string_of_id id)
+       | _ -> bad_vernac_args "ImportModule")
+
+let _ =
   add "PrintModules"
     (function 
        | [] -> 
 	   (fun () ->
               let opened = Library.opened_modules ()
 	      and loaded = Library.loaded_modules () in
-              mSG [< 'sTR"Imported (open) Modules: " ;
+              mSG [< 'sTR"Loaded Modules: ";
+		     hOV 0 (prlist_with_sep pr_fnl 
+			      (fun s -> [< 'sTR s >]) loaded);
+		     'fNL;
+		     'sTR"Imported (open) Modules: ";
 		     hOV 0 (prlist_with_sep pr_fnl
-			      (fun s -> [< 'sTR s >]) opened) ; 
-		     'fNL ;
-		     'sTR"Loaded Modules: " ;
-		     hOV 0 (prlist_with_sep pr_fnl
-			      (fun s -> [< 'sTR s >]) loaded) ;
+			      (fun s -> [< 'sTR s >]) opened); 
 		     'fNL >])
        | _ -> bad_vernac_args "PrintModules")
 
@@ -733,7 +750,6 @@ let _ =
 	   in 
 	   fun () ->
 	     definition_body_red id stre c red_option;
-	     message ((string_of_id id) ^ " is defined");
              if coe then begin
 	       Class.try_add_new_coercion id stre;
                message ((string_of_id id) ^ " is now a coercion")
@@ -1040,20 +1056,14 @@ let _ =
   add "SyntaxMacro"
     (function 
        | [VARG_IDENTIFIER id;VARG_COMMAND com] ->
-	   (fun () -> 
-	      syntax_definition id com;
-              if not(is_silent()) then
-                message ((string_of_id id) ^ " is now a syntax macro"))
+	   (fun () -> syntax_definition id com)
        | [VARG_IDENTIFIER id;VARG_COMMAND com; VARG_NUMBER n] ->
            (fun () ->
               let rec aux t = function
                 | 0 -> t
-               	| n -> aux (ope("APPLIST",
-                               	[t;ope("ISEVAR",[])])) (n-1)
+               	| n -> aux (ope("APPLIST",[t;ope("ISEVAR",[])])) (n-1)
               in 
-	      syntax_definition id (aux com n);
-              if not(is_silent()) then
-                message ((string_of_id id) ^ " is now a syntax macro"))
+	      syntax_definition id (aux com n))
        | _ -> bad_vernac_args "SyntaxMacro")
 
 (***