modules profile, Coqinit et Coqtop (=main)

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

26 files changed, 1394 insertions, 248 deletions

diff --git a/.depend b/.depend
index 96a6e61be..17ae5aaf8 100644
--- a/.depend
+++ b/.depend
@@ -32,6 +32,7 @@ kernel/typeops.cmi: kernel/environ.cmi kernel/evd.cmi kernel/names.cmi \
 kernel/univ.cmi: kernel/names.cmi lib/pp.cmi 
 lib/gmapl.cmi: lib/gmap.cmi 
 lib/pp.cmi: lib/pp_control.cmi 
+lib/system.cmi: lib/pp.cmi 
 lib/util.cmi: lib/pp.cmi 
 library/declare.cmi: kernel/constant.cmi kernel/environ.cmi \
     kernel/inductive.cmi kernel/names.cmi kernel/sign.cmi kernel/term.cmi 
@@ -151,12 +152,14 @@ toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \
 toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \
     pretyping/tacred.cmi kernel/term.cmi 
 toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
+toplevel/fhimsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
+    kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
 toplevel/himsg.cmi: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \
     kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi 
 toplevel/metasyntax.cmi: parsing/coqast.cmi parsing/extend.cmi 
 toplevel/mltop.cmi: library/libobject.cmi 
 toplevel/protectedtoplevel.cmi: lib/pp.cmi 
-toplevel/record.cmi: kernel/names.cmi kernel/term.cmi 
+toplevel/record.cmi: parsing/coqast.cmi kernel/names.cmi kernel/term.cmi 
 toplevel/searchisos.cmi: library/libobject.cmi kernel/names.cmi \
     kernel/term.cmi 
 toplevel/toplevel.cmi: parsing/pcoq.cmi lib/pp.cmi 
@@ -185,12 +188,12 @@ kernel/constant.cmx: kernel/generic.cmx kernel/names.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/univ.cmx kernel/constant.cmi 
 kernel/environ.cmo: kernel/abstraction.cmi kernel/constant.cmi \
     kernel/generic.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
-    kernel/sign.cmi lib/system.cmi kernel/term.cmi kernel/univ.cmi \
-    lib/util.cmi kernel/environ.cmi 
+    kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
+    kernel/environ.cmi 
 kernel/environ.cmx: kernel/abstraction.cmx kernel/constant.cmx \
     kernel/generic.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
-    kernel/sign.cmx lib/system.cmx kernel/term.cmx kernel/univ.cmx \
-    lib/util.cmx kernel/environ.cmi 
+    kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
+    kernel/environ.cmi 
 kernel/evd.cmo: kernel/environ.cmi kernel/names.cmi kernel/sign.cmi \
     kernel/term.cmi lib/util.cmi kernel/evd.cmi 
 kernel/evd.cmx: kernel/environ.cmx kernel/names.cmx kernel/sign.cmx \
@@ -285,6 +288,8 @@ lib/pp.cmo: lib/pp_control.cmi lib/pp.cmi
 lib/pp.cmx: lib/pp_control.cmx lib/pp.cmi 
 lib/pp_control.cmo: lib/pp_control.cmi 
 lib/pp_control.cmx: lib/pp_control.cmi 
+lib/profile.cmo: lib/system.cmi lib/profile.cmi 
+lib/profile.cmx: lib/system.cmx lib/profile.cmi 
 lib/stamps.cmo: lib/stamps.cmi 
 lib/stamps.cmx: lib/stamps.cmi 
 lib/system.cmo: lib/pp.cmi lib/util.cmi lib/system.cmi 
@@ -753,15 +758,39 @@ toplevel/command.cmx: parsing/ast.cmx parsing/astterm.cmx kernel/constant.cmx \
     library/library.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
     library/states.cmx pretyping/syntax_def.cmx pretyping/tacred.cmx \
     kernel/term.cmx lib/util.cmx toplevel/command.cmi 
+toplevel/coqinit.cmo: config/coq_config.cmi toplevel/mltop.cmi \
+    lib/options.cmi lib/pp.cmi lib/system.cmi toplevel/toplevel.cmi \
+    toplevel/vernac.cmi toplevel/coqinit.cmi 
+toplevel/coqinit.cmx: config/coq_config.cmx toplevel/mltop.cmx \
+    lib/options.cmx lib/pp.cmx lib/system.cmx toplevel/toplevel.cmx \
+    toplevel/vernac.cmx toplevel/coqinit.cmi 
+toplevel/coqtop.cmo: config/coq_config.cmi toplevel/coqinit.cmi \
+    toplevel/himsg.cmi library/library.cmi toplevel/mltop.cmi lib/options.cmi \
+    lib/pp.cmi parsing/printer.cmi lib/profile.cmi library/states.cmi \
+    lib/system.cmi toplevel/toplevel.cmi toplevel/usage.cmi lib/util.cmi \
+    toplevel/vernac.cmi 
+toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
+    toplevel/himsg.cmx library/library.cmx toplevel/mltop.cmx lib/options.cmx \
+    lib/pp.cmx parsing/printer.cmx lib/profile.cmx library/states.cmx \
+    lib/system.cmx toplevel/toplevel.cmx toplevel/usage.cmx lib/util.cmx \
+    toplevel/vernac.cmx 
 toplevel/errors.cmo: parsing/ast.cmi lib/options.cmi lib/pp.cmi lib/util.cmi \
     toplevel/errors.cmi 
 toplevel/errors.cmx: parsing/ast.cmx lib/options.cmx lib/pp.cmx lib/util.cmx \
     toplevel/errors.cmi 
-toplevel/himsg.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
+toplevel/fhimsg.cmo: kernel/environ.cmi kernel/generic.cmi kernel/names.cmi \
     lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
-    kernel/type_errors.cmi lib/util.cmi toplevel/himsg.cmi 
-toplevel/himsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
+    kernel/type_errors.cmi lib/util.cmi toplevel/fhimsg.cmi 
+toplevel/fhimsg.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \
     lib/pp.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
+    kernel/type_errors.cmx lib/util.cmx toplevel/fhimsg.cmi 
+toplevel/himsg.cmo: parsing/ast.cmi kernel/environ.cmi kernel/generic.cmi \
+    parsing/lexer.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
+    parsing/printer.cmi kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \
+    kernel/type_errors.cmi lib/util.cmi toplevel/himsg.cmi 
+toplevel/himsg.cmx: parsing/ast.cmx kernel/environ.cmx kernel/generic.cmx \
+    parsing/lexer.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
+    parsing/printer.cmx kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx lib/util.cmx toplevel/himsg.cmi 
 toplevel/metasyntax.cmo: parsing/ast.cmi parsing/coqast.cmi \
     parsing/egrammar.cmi parsing/esyntax.cmi parsing/extend.cmi \
@@ -773,12 +802,12 @@ toplevel/metasyntax.cmx: parsing/ast.cmx parsing/coqast.cmx \
     library/lib.cmx library/libobject.cmx library/library.cmx \
     parsing/pcoq.cmi lib/pp.cmx library/summary.cmx lib/util.cmx \
     toplevel/metasyntax.cmi 
-toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \
-    kernel/generic.cmi toplevel/himsg.cmi kernel/inductive.cmi \
+toplevel/minicoq.cmo: kernel/constant.cmi toplevel/fhimsg.cmi \
+    parsing/g_minicoq.cmi kernel/generic.cmi kernel/inductive.cmi \
     kernel/names.cmi lib/pp.cmi kernel/safe_typing.cmi kernel/sign.cmi \
     kernel/term.cmi kernel/type_errors.cmi lib/util.cmi 
-toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \
-    kernel/generic.cmx toplevel/himsg.cmx kernel/inductive.cmx \
+toplevel/minicoq.cmx: kernel/constant.cmx toplevel/fhimsg.cmx \
+    parsing/g_minicoq.cmi kernel/generic.cmx kernel/inductive.cmx \
     kernel/names.cmx lib/pp.cmx kernel/safe_typing.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/type_errors.cmx lib/util.cmx 
 toplevel/mltop.cmo: library/lib.cmi library/libobject.cmi library/library.cmi \
@@ -793,10 +822,12 @@ toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \
 toplevel/protectedtoplevel.cmx: toplevel/errors.cmx parsing/pcoq.cmi \
     lib/pp.cmx toplevel/vernac.cmx toplevel/vernacinterp.cmx \
     toplevel/protectedtoplevel.cmi 
-toplevel/record.cmo: toplevel/class.cmi library/declare.cmi kernel/names.cmi \
-    kernel/term.cmi lib/util.cmi toplevel/record.cmi 
-toplevel/record.cmx: toplevel/class.cmx library/declare.cmx kernel/names.cmx \
-    kernel/term.cmx lib/util.cmx toplevel/record.cmi 
+toplevel/record.cmo: parsing/ast.cmi toplevel/class.cmi parsing/coqast.cmi \
+    library/declare.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi \
+    lib/util.cmi toplevel/record.cmi 
+toplevel/record.cmx: parsing/ast.cmx toplevel/class.cmx parsing/coqast.cmx \
+    library/declare.cmx kernel/names.cmx lib/pp.cmx kernel/term.cmx \
+    lib/util.cmx toplevel/record.cmi 
 toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi toplevel/mltop.cmi \
     lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
     toplevel/protectedtoplevel.cmi lib/util.cmi toplevel/vernac.cmi \
@@ -805,6 +836,8 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx toplevel/mltop.cmx \
     lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx lib/pp.cmx \
     toplevel/protectedtoplevel.cmx lib/util.cmx toplevel/vernac.cmx \
     toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
+toplevel/usage.cmo: toplevel/usage.cmi 
+toplevel/usage.cmx: toplevel/usage.cmi 
 toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
     lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
     library/states.cmi lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi \
@@ -814,29 +847,29 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
     library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
-    toplevel/command.cmi parsing/coqast.cmi library/declare.cmi \
-    kernel/environ.cmi kernel/evd.cmi parsing/extend.cmi library/global.cmi \
-    library/goptions.cmi library/impargs.cmi library/lib.cmi \
-    library/libobject.cmi library/library.cmi proofs/macros.cmi \
-    toplevel/metasyntax.cmi kernel/names.cmi library/nametab.cmi \
-    lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
-    lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \
+    toplevel/class.cmi toplevel/command.cmi parsing/coqast.cmi \
+    library/declare.cmi kernel/environ.cmi kernel/evd.cmi parsing/extend.cmi \
+    library/global.cmi library/goptions.cmi library/impargs.cmi \
+    library/lib.cmi library/libobject.cmi library/library.cmi \
+    proofs/macros.cmi toplevel/metasyntax.cmi kernel/names.cmi \
+    library/nametab.cmi lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi \
+    lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi parsing/printer.cmi \
     proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \
     lib/stamps.cmi library/states.cmi lib/system.cmi proofs/tacmach.cmi \
-    kernel/term.cmi kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
-    toplevel/vernacentries.cmi 
+    pretyping/tacred.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
+    toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
-    toplevel/command.cmx parsing/coqast.cmx library/declare.cmx \
-    kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi library/global.cmx \
-    library/goptions.cmx library/impargs.cmx library/lib.cmx \
-    library/libobject.cmx library/library.cmx proofs/macros.cmx \
-    toplevel/metasyntax.cmx kernel/names.cmx library/nametab.cmx \
-    lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx lib/pp.cmx \
-    lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \
+    toplevel/class.cmx toplevel/command.cmx parsing/coqast.cmx \
+    library/declare.cmx kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi \
+    library/global.cmx library/goptions.cmx library/impargs.cmx \
+    library/lib.cmx library/libobject.cmx library/library.cmx \
+    proofs/macros.cmx toplevel/metasyntax.cmx kernel/names.cmx \
+    library/nametab.cmx lib/options.cmx parsing/pcoq.cmi proofs/pfedit.cmx \
+    lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx parsing/printer.cmx \
     proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \
     lib/stamps.cmx library/states.cmx lib/system.cmx proofs/tacmach.cmx \
-    kernel/term.cmx kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
-    toplevel/vernacentries.cmi 
+    pretyping/tacred.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
+    toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
 toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \
     toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
     proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \
diff --git a/Makefile b/Makefile
index e69874b8d..a492fd0c6 100644
--- a/Makefile
+++ b/Makefile
@@ -34,7 +34,7 @@ CONFIG=config/coq_config.cmo
 LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \
     lib/hashcons.cmo lib/dyn.cmo lib/system.cmo lib/options.cmo \
     lib/bstack.cmo lib/edit.cmo lib/stamps.cmo lib/gset.cmo lib/gmap.cmo \
-    lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo
+    lib/tlm.cmo lib/bij.cmo lib/gmapl.cmo lib/profile.cmo
 
 KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
        kernel/sign.cmo kernel/constant.cmo \
@@ -77,7 +77,8 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
          toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \
          toplevel/vernacentries.cmo toplevel/vernac.cmo toplevel/mltop.cmo \
-	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo
+	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo \
+         toplevel/usage.cmo toplevel/coqinit.cmo toplevel/coqtop.cmo
 
 CMA=$(CLIBS) $(CAMLP4OBJS)
 CMXA=$(CMA:.cma=.cmxa)
@@ -118,7 +119,7 @@ coqtop.byte: $(CMO) Makefile
 
 MINICOQCMO=$(CONFIG) $(LIB) $(KERNEL) \
 	   parsing/lexer.cmo parsing/g_minicoq.cmo \
-	   toplevel/himsg.cmo toplevel/minicoq.cmo
+	   toplevel/fhimsg.cmo toplevel/minicoq.cmo
 
 minicoq: $(MINICOQCMO)
 	$(OCAMLC) $(INCLUDES) -o minicoq -custom $(CMA) $(MINICOQCMO) \
diff --git a/configure b/configure
index 0cdd5f36a..ee493b3dd 100755
--- a/configure
+++ b/configure
@@ -6,7 +6,7 @@
 # 
 ##################################
 
-VERSION=7.0
+VERSION=7.00
 VERSIONSI=1.0
 DATE="August 1999"
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a6e878e6b..5ac91dc00 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -2,7 +2,6 @@
 (* $Id$ *)
 
 open Pp
-open System
 open Util
 open Names
 open Sign
@@ -15,7 +14,9 @@ open Abstraction
 
 (* The type of environments. *)
 
-type import = string * time_stamp
+type checksum = int
+
+type import = string * checksum
 
 type global = Constant | Inductive | Abstraction
 
@@ -217,7 +218,7 @@ let evaluable_constant env k =
 
 type compiled_env = {
   cenv_id : string;
-  cenv_stamp : time_stamp;
+  cenv_stamp : checksum;
   cenv_needed : import list;
   cenv_constants : (section_path * constant_body) list;
   cenv_inductives : (section_path * mutual_inductive_body) list;
@@ -235,7 +236,7 @@ let exported_objects env =
 let export env id = 
   let (cst,ind,abs) = exported_objects env in
   { cenv_id = id;
-    cenv_stamp = get_time_stamp ();
+    cenv_stamp = 0;
     cenv_needed = env.env_globals.env_imports;
     cenv_constants = cst;
     cenv_inductives = ind;
@@ -246,7 +247,7 @@ let check_imports env needed =
   let check (id,stamp) =
     try
       let actual_stamp = List.assoc id imports in
-      if compare_time_stamps stamp actual_stamp <> 0 then
+      if stamp <> actual_stamp then
 	error ("Inconsistent assumptions over module " ^ id)
     with Not_found -> 
       error ("Reference to unknown module " ^ id)
diff --git a/lib/profile.ml b/lib/profile.ml
new file mode 100644
index 000000000..3e1d04607
--- /dev/null
+++ b/lib/profile.ml
@@ -0,0 +1,311 @@
+
+(* $Id$ *)
+
+(* This program is a small time-profiler for Caml-Special-Light *)
+
+(* It requires the UNIX library *)
+
+(* Adapted from Christophe Raffalli *)
+
+(* To use it, link it with the program you want to profile (don not forget
+"-cclib -lunix -custom unix.cma" among the link options).
+
+To trace a function "f" you first need to get a key for it by using :
+
+let fkey = declare_profile "f"
+
+(the string is used to print the profile infomation). Warning: this
+function does a side effect. Choose the ident you want instead "fkey".
+
+Then if the function has one ONE argument add the following just after
+the definition of "f" or just after the declare_profile if this one
+follows the defintion of f.
+
+let f = profile fkey f
+
+If f has two arguments do the same with profile2, idem with 3 and
+4. For more than 4 arguments ... modify the function profile yourself,
+it is very easy (look the differences between profile and profile2.
+
+If you want to profile two mutually recursive functions, you had better
+to rename them :
+
+let fkey = declare_profile "f"
+let gkey = declare_profile "g"
+let f' = .... f' ... g'
+and g' = .... f' .... g'
+
+
+let f = profile fkey f'
+let g = profile gkey g'
+
+Before the program quits, you should call "print_profile ()". It
+produces a result of the following kind:
+
+f 5.32 7.10
+g 4.00 4.00
+main 0.12 9.44
+total -9.44 0.00
+
+- The first column is the name of the function.
+
+- The third column give the time (utime + stime) spend inside the function.
+
+- The second column give the time spend inside the function minus the
+time spend in other profiled functions called by it
+
+The last line can be ignored (there is a bug if the down-right digit is non
+zero)
+
+*)
+
+type profile_key = float ref * float ref
+
+let actif = ref true
+
+let tot_ptr = ref 0.0 and tot_ptr' = ref 0.0
+
+let prof_table = ref ["total",(tot_ptr,tot_ptr')]
+
+let stack = ref [tot_ptr']
+
+let ajoute ((name,(ptr1,ptr1')) as e) l =
+  try let (ptr,ptr') = List.assoc name l in
+  ptr  := !ptr  +. !ptr1;
+  ptr' := !ptr' +. !ptr1';
+  l
+  with Not_found -> e::l
+
+
+let magic = 1248
+
+let append_profile name =
+  if List.length !prof_table <> 1 then begin
+    let prof_table =
+      if name = "" then !prof_table
+      else
+	let new_prof_table =
+          try 
+            let c = open_in name in
+            if input_binary_int c <> magic 
+            then Printf.printf "Bad already existing recording file\n";
+            let old_prof_table = input_value c in
+            close_in c;
+            List.fold_right ajoute !prof_table old_prof_table
+          with Sys_error _ ->
+            (Printf.printf "Non existent or unaccessible recording file\n";
+             !prof_table)
+	in begin
+          (try
+             let c = open_out_gen 
+                       [Open_creat;Open_wronly;Open_trunc;Open_binary] 0o644 name in
+             output_binary_int c magic;
+             output_value c new_prof_table;
+             close_out c
+           with Sys_error _ -> Printf.printf "Unable to create recording file");
+            new_prof_table
+	  end
+    in
+    print_newline ();
+    Printf.printf "%-25s  %11s  %11s\n" 
+      "Function name" "Proper time" "Total time";
+    let l = Sort.list (fun (_,(_,p)) (_,(_,p')) -> !p > !p') prof_table in
+    List.iter (fun (name,(ptr,ptr')) ->
+		 Printf.printf "%-25s  %11.2f  %11.2f\n" name !ptr' !ptr) l;
+    Gc.print_stat stdout
+  end
+
+
+let recording_file = ref ""
+let set_recording s = recording_file := s
+
+let print_profile () = append_profile !recording_file
+
+let reset_profile () = 
+  List.iter (fun (name,(p,p')) -> p:=0.0; p':=0.0) !prof_table
+
+let init_profile () = 
+  tot_ptr:= 0.0; tot_ptr':=0.0; prof_table :=["total",(tot_ptr,tot_ptr')] 
+
+let declare_profile name = let ptr = ref 0.0 and ptr' = ref 0.0 in
+prof_table := (name,(ptr,ptr'))::!prof_table;(ptr,ptr')
+
+let profile (ptr,ptr') f =
+  (fun x ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile2 (ptr,ptr') f =
+  (fun x y ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile3 (ptr,ptr') f =
+  (fun x y z ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y z in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile4 (ptr,ptr') f =
+  (fun x y z t ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y z t in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile5 (ptr,ptr') f =
+  (fun x y z t u ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y z t u in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile6 (ptr,ptr') f =
+  (fun x y z t u v ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y z t u v in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
+
+
+
+let profile7 (ptr,ptr') f =
+  (fun x y z t u v w ->
+     let (ut,st) = System.process_time () in
+     stack := ptr'::!stack;
+     try
+       let r = f x y z t u v w in
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       r
+     with e ->
+       let (ut',st') = System.process_time () in
+       let t = (ut' -. ut) +. (st' -. st) in
+       (match !stack with
+	    _::(ptr'::_ as s) -> stack:=s; ptr' := !ptr' -. t
+	  | _ -> failwith "bug in profile");
+       ptr := !ptr +. t;
+       ptr' := !ptr' +. t;
+       raise e)
diff --git a/lib/profile.mli b/lib/profile.mli
new file mode 100644
index 000000000..893bf07b9
--- /dev/null
+++ b/lib/profile.mli
@@ -0,0 +1,29 @@
+
+(* $Id$ *)
+
+(* Profiling. *)
+
+type profile_key
+
+val actif : bool ref
+val print_profile : unit -> unit
+val reset_profile : unit -> unit
+val init_profile : unit -> unit
+val declare_profile : string -> profile_key
+val profile : profile_key -> ('a -> 'b) -> 'a -> 'b
+val profile2 : profile_key -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c
+val profile3 :
+  profile_key -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
+val profile4 :
+  profile_key -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e
+val profile5 :
+  profile_key ->
+  ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f
+val profile6 :
+  profile_key ->
+  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g)
+    -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g
+val profile7 :
+  profile_key ->
+  ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) 
+    -> 'a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h
diff --git a/lib/system.ml b/lib/system.ml
index 9da302d30..5422bc465 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -44,7 +44,14 @@ let all_subdirs dir =
 
 let radd_path dir = List.iter add_path (all_subdirs dir)
 
+let safe_getenv_def var def =
+  try 
+    Sys.getenv var
+  with Not_found ->
+    warning ("Environnement variable "^var^" not found: using '"^def^"' .");
+    def
 
+let home = (safe_getenv_def "HOME" ".")
 
 (* TODO: rétablir glob (expansion ~user et $VAR) si on le juge nécessaire *)
 let glob s = s
@@ -82,6 +89,9 @@ let is_in_path lpath filename =
 let make_suffix name suffix =
   if Filename.check_suffix name suffix then name else (name ^ suffix)
 
+let file_readable_p na =
+  try access (glob na) [R_OK];true with Unix_error (_, _, _) -> false
+
 let open_trapping_failure open_fun name suffix =
   let rname = make_suffix name suffix in
   try open_fun rname with _ -> error ("Can't open " ^ rname)
@@ -141,11 +151,22 @@ let (extern_intern :
 
 (* Time stamps. *)
 
-type time_stamp = float
-
-let get_time_stamp () = Unix.time()
-
-let compare_time_stamps t1 t2 =
-  let dt = t2 -. t1 in
-  if dt < 0.0 then -1 else if dt = 0.0 then 0 else 1
-
+type time = float * float * float
+
+let process_time () = 
+  let t = times ()  in
+  (t.tms_utime, t.tms_stime)
+
+let get_time () = 
+  let t = times ()  in
+  (time(), t.tms_utime, t.tms_stime)
+
+let time_difference (t1,_,_) (t2,_,_) = t2 -. t1
+			      
+let fmt_time_difference (startreal,ustart,sstart) (stopreal,ustop,sstop) =
+  [< 'rEAL(stopreal -. startreal); 'sTR" secs ";
+     'sTR"(";
+     'rEAL((-.) ustop ustart); 'sTR"u";
+     'sTR",";
+     'rEAL((-.) sstop sstart); 'sTR"s";
+     'sTR")" >]
diff --git a/lib/system.mli b/lib/system.mli
index 0c4bbd228..e3fd5978c 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -8,9 +8,12 @@ val is_in_path : string list -> string -> bool
 val where_in_path : string list -> string -> string
 
 val make_suffix : string -> string -> string
+val file_readable_p : string -> bool
 
 val glob : string -> string
 
+val home : string
+
 (*s Global load path. *)
 
 val add_path : string -> unit
@@ -34,8 +37,11 @@ val extern_intern : int -> string -> (string -> 'a -> unit) * (string -> 'a)
 
 (*s Time stamps. *)
 
-type time_stamp
+type time
+
+val process_time : unit -> float * float
+val get_time : unit -> time
+val time_difference : time -> time -> float (* in seconds *)
+val fmt_time_difference : time -> time -> Pp.std_ppcmds
 
-val get_time_stamp : unit -> time_stamp
-val compare_time_stamps : time_stamp -> time_stamp -> int
 
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index b8046716c..469e61393 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -1,6 +1,8 @@
 
 (* $Id$ *)
 
+exception BadToken of string
+
 val add_keyword : string -> unit
 val is_keyword : string -> bool
 val find_keyword : string -> string
diff --git a/parsing/lexer.mll b/parsing/lexer.mll
index 0eaa87f93..5cb993b26 100644
--- a/parsing/lexer.mll
+++ b/parsing/lexer.mll
@@ -9,6 +9,8 @@ type error =
   | Unterminated_comment
   | Unterminated_string
 
+exception BadToken of string
+
 exception Error of error * int * int
 
 type frozen_t = string list
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 96f282cac..a87f15deb 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -22,6 +22,8 @@ val fterm0          : 'a assumptions -> constr -> std_ppcmds
 val term0           : 'a assumptions -> constr -> std_ppcmds
 val term0_at_top    : 'a assumptions -> constr -> std_ppcmds
 
+val pr_ne_env       : std_ppcmds -> path_kind -> context -> std_ppcmds
+
 val prrawterm       : Rawterm.rawconstr -> std_ppcmds
 val prpattern       : Rawterm.pattern -> std_ppcmds
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 3e86b3862..966630eae 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -66,3 +66,4 @@ val make_focus : int -> unit
 val focus : unit -> int
 val focused_goal : unit -> int
 
+val subtree_solved : unit -> bool
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 1c4287169..d36b162ad 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -152,6 +152,7 @@ val dyn_cut_and_apply     : tactic_arg list -> tactic
 (*s Instantiation tactics. *)
 
 val instantiate_pf     : int -> constr -> pftreestate -> pftreestate
+val instantiate_pf_com : int -> Coqast.t -> pftreestate -> pftreestate
 
 (*s Elimination tactics. *)
 
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
new file mode 100644
index 000000000..4d2a44262
--- /dev/null
+++ b/toplevel/coqinit.ml
@@ -0,0 +1,79 @@
+
+(* $Id$ *)
+
+open Pp
+open System
+open Toplevel
+
+let set_debug () = Options.debug := true
+
+(* Load of rcfile.
+ * rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one
+ * does not exist. *)
+
+let rcfile = ref (Filename.concat home ".coqrc")
+let rcfile_specified = ref false
+let set_rcfile s = rcfile := s; rcfile_specified := true
+let set_rcuser s = rcfile := Filename.concat ("~"^s) ".coqrc"
+
+let load_rc = ref true
+let no_load_rc () = load_rc := false
+
+let load_rcfile() =
+  if !load_rc then
+    try
+      if !rcfile_specified then
+        if file_readable_p !rcfile then 
+          Vernac.load_vernac false !rcfile
+        else raise (Sys_error ("Cannot read rcfile: "^ !rcfile))
+      else if file_readable_p (!rcfile^"."^Coq_config.version) then
+        Vernac.load_vernac false (!rcfile^"."^Coq_config.version)
+      else if file_readable_p !rcfile then
+        Vernac.load_vernac false !rcfile
+      else mSGNL [< 'sTR ("No .coqrc or .coqrc."^Coq_config.version^
+		   " found. Skipping rcfile loading.") >]
+    with e ->
+      (mSGNL [< 'sTR"Load of rcfile failed." >];
+       raise e)
+  else mSGNL [< 'sTR"Skipping rcfile loading." >]
+
+(*Puts dir in the path of ML and in the LoadPath*)
+let add_include s =
+  Mltop.dir_ml_dir s;
+  add_path s
+
+(*By the option -include -I or -R of the command line*)
+let includes = ref []
+let push_include s = includes := s :: !includes
+let rec_include s = includes := (all_subdirs s)@(!includes)
+
+(*Because find puts "./" and the loadpath is not really pretty-printed*)
+let hm2 str=
+  String.sub str 2 ((String.length str)-2)
+
+(*Initializes the LoadPath according to COQLIB and Coq_config*)
+let init_load_path () =
+  (* default load path; only if COQLIB is defined *)
+  begin
+    try
+      let coqlib = Sys.getenv "COQLIB" in
+      if coqlib <> "" then
+      	List.iter
+	  (fun s -> add_include (Filename.concat coqlib s))
+      	  ("states" :: 
+	   (List.map (fun s -> Filename.concat "theories" (hm2 s))
+             Coq_config.theories_dirs))
+    with Not_found -> ()
+  end ;
+
+  begin
+    try
+      let camlp4 = Sys.getenv "CAMLP4LIB" in add_include camlp4
+    with Not_found -> ()
+  end ;
+
+  add_include "." ;
+
+  (* additional loadpath, given with -I -include -R options *)
+  List.iter add_include (List.rev !includes);
+  includes := []
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
new file mode 100644
index 000000000..ca74f9ec7
--- /dev/null
+++ b/toplevel/coqinit.mli
@@ -0,0 +1,20 @@
+
+(* $Id$ *)
+
+(* Initialization. *)
+
+val set_debug : unit -> unit
+
+val set_rcfile : string -> unit
+val set_rcuser : string -> unit
+
+val no_load_rc : unit -> unit
+val load_rcfile : unit -> unit
+
+val add_include : string -> unit
+val push_include : string -> unit
+val rec_include : string -> unit
+
+val hm2 : string -> string
+
+val init_load_path : unit -> unit
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
new file mode 100644
index 000000000..a056ca8fc
--- /dev/null
+++ b/toplevel/coqtop.ml
@@ -0,0 +1,166 @@
+
+(* $Id$ *)
+
+(* The Coq main module. *)
+
+open Pp
+open Util
+open System
+open Options
+open States
+open Toplevel
+open Coqinit
+
+let print_header () =
+  Printf.printf "Welcome to Coq %s (%s)\n" Coq_config.version Coq_config.date;
+  flush stdout
+
+let batch_mode = ref false
+let set_batch_mode () = batch_mode := true
+
+let remove_top_ml () = Mltop.remove ()
+
+let inputstate = ref "tactics.coq"
+let set_inputstate s = inputstate:= s
+let inputstate () =if !inputstate <> "" then intern_state !inputstate
+
+let outputstate = ref ""
+let set_outputstate s = outputstate:=s
+let outputstate () = if !outputstate <> "" then extern_state !outputstate
+
+let load_vernacular_list = ref ([]:string list)
+let add_load_vernacular s =
+  load_vernacular_list := (make_suffix s ".v")::(!load_vernacular_list)
+let load_vernacular () =
+  List.iter
+    (fun s -> Vernac.load_vernac false s)
+    (List.rev !load_vernacular_list)
+
+let load_vernacular_obj = ref ([]:string list)
+let add_vernac_obj s = load_vernacular_obj := s::(!load_vernacular_obj)
+let load_vernac_obj () = 
+  List.iter
+    (fun s -> Library.load_module (Filename.basename s) (Some s))
+    (List.rev !load_vernacular_obj)
+
+let require_list = ref ([]:string list)
+let add_require s = require_list := s::(!require_list)
+let require () =
+  List.iter
+    (fun s -> Library.require_module None (Filename.basename s) (Some s) false)
+    (List.rev !require_list)
+
+
+(*
+ * 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.
+ *)
+
+let usage () =
+  if !batch_mode then
+    Usage.print_usage_coqc ()
+  else
+    Usage.print_usage_coqtop () ;
+  flush stderr ;
+  exit 1
+
+
+let parse_args () =
+  let rec parse = function
+    | [] -> ()
+
+    | ("-I"|"-include") :: d :: rem -> push_include d ; parse rem
+    | ("-I"|"-include") :: []       -> usage ()
+
+    | ("-R") :: d :: rem -> rec_include d ; parse rem
+    | ("-R") :: []       -> usage ()
+
+    | "-q" :: rem -> no_load_rc () ; parse rem
+
+    | "-batch" :: rem -> set_batch_mode () ; parse rem
+	     
+    | "-outputstate" :: s :: rem -> set_outputstate s ; parse rem
+    | "-outputstate" :: []       -> usage ()
+
+    | "-nois" :: rem -> set_inputstate "" ; 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" :: []       -> usage ()
+
+    | "-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" :: []       -> usage ()
+
+    | "-load-vernac-object" :: f :: rem -> add_vernac_obj f ; parse rem
+    | "-load-vernac-object" :: []       -> usage ()
+
+    | "-require" :: f :: rem -> add_require f ; parse rem
+    | "-require" :: []       -> usage ()
+
+    | "-unsafe" :: f :: rem -> add_unsafe f ; parse rem
+    | "-unsafe" :: []       -> usage ()
+
+    | "-debug" :: rem -> set_debug () ; parse rem
+
+    | "-emacs" :: rem -> Printer.print_emacs := true ; parse rem
+
+    | "-init-file" :: f :: rem -> set_rcfile f ; parse rem
+    | "-init-file" :: []       -> usage ()
+
+    | "-user" :: u :: rem -> set_rcuser u ; parse rem
+    | "-user" :: []       -> usage ()
+
+    | "-notactics" :: rem -> remove_top_ml () ; parse rem
+
+    | "-just-parsing" :: rem -> Vernac.just_parsing := true ; parse rem
+
+    | s :: _ -> prerr_endline ("Don't know what to do with " ^ s) ; usage ()
+
+  in
+  try
+    parse (List.tl (Array.to_list Sys.argv))
+  with 
+    | UserError(_,s) as e -> begin
+	try
+	  Stream.empty s; exit 1
+	with Stream.Failure ->
+	  mSGNL (Himsg.explain_error e); exit 1
+      end
+    | e -> begin mSGNL (Himsg.explain_error e); exit 1 end
+
+
+(* To prevent from doing the initialization twice *)
+let initialized = ref false
+
+(* Ctrl-C is fatal during the initialisation *)
+let start () =
+  if not !initialized then begin
+    initialized := true;
+    Sys.catch_break false;
+    try
+      parse_args ();
+      print_header ();
+      init_load_path ();
+      inputstate ();
+      load_vernac_obj ();
+      require ();
+      load_rcfile();
+      load_vernacular ();
+      outputstate ()
+    with e ->
+      flush_all();
+      if not !batch_mode then message "Error during initialization :";
+      mSGNL (Toplevel.print_toplevel_error e);
+      exit 1
+  end;
+  if !batch_mode then (flush_all(); Profile.print_profile ();exit 0);
+  Toplevel.loop()
+
+let _ = start()
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
new file mode 100644
index 000000000..419488a37
--- /dev/null
+++ b/toplevel/fhimsg.ml
@@ -0,0 +1,292 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Sign
+open Environ
+open Type_errors
+open Reduction
+
+module type Printer = sig
+  val pr_term : path_kind -> context -> constr -> std_ppcmds
+end
+
+module Make = functor (P : Printer) -> struct
+
+  let print_decl k sign (s,typ) =
+    let ptyp = P.pr_term k (gLOB sign) typ.body in 
+    [< 'sPC; print_id s; 'sTR" : "; ptyp >]
+  
+  let print_binding k env = function
+    | Anonymous,ty -> 
+	[< 'sPC; 'sTR"_" ; 'sTR" : " ; P.pr_term k env ty.body >]
+    | Name id,ty -> 
+	[< 'sPC; print_id id ; 'sTR" : "; P.pr_term k env ty.body >]
+
+  let sign_it_with f sign e =
+    snd (sign_it 
+	   (fun id t (sign,e) -> (add_sign (id,t) sign, f id t sign e))
+           sign (nil_sign,e))
+
+  let dbenv_it_with f env e =
+    snd (dbenv_it 
+	   (fun na t (env,e) -> (add_rel (na,t) env, f na t env e))
+           env (gLOB(get_globals env),e))
+      
+  let pr_env k env =
+    let sign_env =
+      sign_it_with
+	(fun id t sign pps ->
+           let pidt =  print_decl k sign (id,t) in [<  pps ; 'fNL ; pidt >])
+	(get_globals env) [< >] 
+    in
+    let db_env =
+      dbenv_it_with 
+	(fun na t env pps ->
+           let pnat = print_binding k env (na,t) in [<  pps ; 'fNL ; pnat >])
+	env [< >]
+    in 
+    [< sign_env; db_env >]
+    
+  let pr_ne_ctx header k = function
+    | ENVIRON (([],[]),[]) -> [< >]
+    | env -> [< header; pr_env k env >]
+
+
+let explain_unbound_rel k ctx n =
+  let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
+  [< 'sTR"Unbound reference: "; pe; 'fNL;
+     'sTR"The reference "; 'iNT n; 'sTR" is free" >]
+
+let explain_cant_execute k ctx c =
+  let tc = P.pr_term k ctx c in
+  [< 'sTR"Cannot execute term:"; 'bRK(1,1); tc >]
+
+let explain_not_type k ctx c =
+  let pe = pr_ne_ctx [< 'sTR"In environment" >] k ctx in
+  let pc = P.pr_term k ctx c in
+  [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
+     'sTR"should be typed by Set, Prop or Type." >];;
+
+let explain_bad_assumption k ctx c =
+  let pc = P.pr_term k ctx c in
+  [< 'sTR "Cannot declare a variable or hypothesis over the term";
+     'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];;
+
+let explain_reference_variables id =
+  [< 'sTR "the constant"; 'sPC; print_id id; 'sPC; 
+     'sTR "refers to variables which are not in the context" >]
+
+let msg_bad_elimination ctx k = function
+  | Some(ki,kp,explanation) ->
+      let pki = P.pr_term k ctx ki in
+      let pkp = P.pr_term k ctx kp in
+      (hOV 0 
+         [< 'fNL; 'sTR "Elimination of an inductive object of sort : ";
+            pki; 'bRK(1,0);
+            'sTR "is not allowed on a predicate in sort : "; pkp ;'fNL;
+            'sTR "because"; 'sPC; 'sTR explanation >])
+  | None -> 
+      [<>]
+
+let explain_elim_arity k ctx ind aritylst c p pt okinds = 
+  let pi = P.pr_term k ctx ind in
+  let ppar = prlist_with_sep pr_coma (P.pr_term k ctx) aritylst in
+  let pc = P.pr_term k ctx c in
+  let pp = P.pr_term k ctx p in
+  let ppt = P.pr_term k ctx pt in
+  [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
+     'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
+     'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
+     'sTR "has type"; 'bRK(1,1); ppt; 'fNL;
+     'sTR "It should be one of :"; 'bRK(1,1) ; hOV 0 ppar; 'fNL;
+     msg_bad_elimination ctx k okinds >]
+
+let explain_case_not_inductive k ctx c ct =
+  let pc = P.pr_term k ctx c in
+  let pct = P.pr_term k ctx ct in
+  [< 'sTR "In Cases expression"; 'bRK(1,1); pc; 'sPC; 
+     'sTR "has type"; 'bRK(1,1); pct; 'sPC; 
+     'sTR "which is not an inductive definition" >]
+  
+let explain_number_branches k ctx c ct expn =
+  let pc = P.pr_term k ctx c in
+  let pct = P.pr_term k ctx ct in
+  [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
+     'sTR "of type"; 'bRK(1,1); pct; 'sPC;
+     'sTR "expects ";  'iNT expn; 'sTR " branches" >]
+
+let explain_ill_formed_branch k ctx c i actty expty =
+  let pc = P.pr_term k ctx c in
+  let pa = P.pr_term k ctx actty in
+  let pe = P.pr_term k ctx expty in
+  [< 'sTR "In Cases expression on term"; 'bRK(1,1); pc;
+     'sPC; 'sTR "the branch " ; 'iNT (i+1);
+     'sTR " has type"; 'bRK(1,1); pa ; 'sPC; 
+     'sTR "which should be:"; 'bRK(1,1); pe >]
+
+let explain_generalization k ctx (name,var) c =
+  let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
+  let pv = P.pr_term k ctx var.body in
+  let pc = P.pr_term k (add_rel (name,var) ctx) c in
+  [< 'sTR"Illegal generalization: "; pe; 'fNL;
+     'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
+     'sTR"over"; 'bRK(1,1); pc; 'sPC;
+     'sTR"which should be typed by Set, Prop or Type." >]
+
+let explain_actual_type k ctx c ct pt =
+  let pe = pr_ne_ctx [< 'sTR"In environment" >] k ctx in
+  let pc = P.pr_term k ctx c in
+  let pct = P.pr_term k ctx ct in
+  let pt = P.pr_term k ctx pt in
+  [< pe; 'fNL;
+     'sTR"The term"; 'bRK(1,1); pc ; 'sPC ;
+     'sTR"does not have type"; 'bRK(1,1); pt; 'fNL;
+     'sTR"Actually, it has type" ; 'bRK(1,1); pct >]
+
+let explain_cant_apply k ctx s rator randl =
+  let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
+  let pr = P.pr_term k ctx rator.uj_val in
+  let prt = P.pr_term k ctx rator.uj_type in
+  let term_string = if List.length randl > 1 then "terms" else "term" in
+  let appl = 
+    prlist_with_sep pr_fnl
+      (fun c ->
+         let pc = P.pr_term k ctx c.uj_val in
+         let pct = P.pr_term k ctx c.uj_type in
+         hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl 
+  in
+  [< 'sTR"Illegal application ("; 'sTR s; 'sTR"): "; pe; 'fNL;
+     'sTR"The term"; 'bRK(1,1); pr; 'sPC;
+     'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
+     'sTR("cannot be applied to the "^term_string); 'fNL; 
+     'sTR" "; v 0 appl >]
+
+(* (co)fixpoints *)
+let explain_ill_formed_rec_body k ctx str lna i vdefs =
+  let pvd = P.pr_term k ctx vdefs.(i) in
+  let s =
+    match List.nth lna i with Name id -> string_of_id id | Anonymous -> "_" in
+  [< str; 'fNL; 'sTR"The ";
+     if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">];
+     'sTR"recursive definition"; 'sPC; 'sTR s;
+	 'sPC ; 'sTR":="; 'sPC ; pvd; 'sPC;
+     'sTR "is not well-formed" >]
+    
+let explain_ill_typed_rec_body k ctx i lna vdefj vargs =
+  let pvd = P.pr_term k ctx (vdefj.(i)).uj_val in
+  let pvdt = P.pr_term k ctx (vdefj.(i)).uj_type in
+  let pv = P.pr_term k ctx (body_of_type vargs.(i)) in
+  [< 'sTR"The " ;
+     if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">];
+     'sTR"recursive definition" ; 'sPC; pvd; 'sPC;
+     'sTR "has type"; 'sPC; pvdt;'sPC; 'sTR "it should be"; 'sPC; pv >]
+
+let explain_not_inductive k ctx c =
+  let pc = P.pr_term k ctx c in
+  [< 'sTR"The term"; 'bRK(1,1); pc; 'sPC;
+     'sTR "is not an inductive definition" >]
+
+let explain_ml_case k ctx mes c ct br brt =
+  let pc = P.pr_term k ctx c in
+  let pct = P.pr_term k ctx ct in
+  let expln =
+    match mes with
+      | "Inductive" -> [< pct; 'sTR "is not an inductive definition">]
+      | "Predicate" -> [< 'sTR "ML case not allowed on a predicate">]
+      | "Absurd" -> [< 'sTR "Ill-formed case expression on an empty type" >]
+      | "Decomp" ->
+          let plf = P.pr_term k ctx br in
+          let pft = P.pr_term k ctx brt in
+          [< 'sTR "The branch "; plf; 'wS 1; 'cUT; 'sTR "has type "; pft;
+             'wS 1; 'cUT;
+             'sTR "does not correspond to the inductive definition" >]
+      | "Dependent" ->
+          [< 'sTR "ML case not allowed for a dependent case elimination">]
+      | _ -> [<>]
+  in
+  hOV 0 [< 'sTR "In ML case expression on "; pc; 'wS 1; 'cUT ;
+           'sTR "of type";  'wS 1; pct; 'wS 1; 'cUT; 
+           'sTR "which is an inductive predicate."; 'fNL; expln >]
+(*
+let explain_cant_find_case_type loc k ctx c =
+  let pe = P.pr_term k ctx c in
+  Ast.user_err_loc
+    (loc,"pretype",
+     hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 
+	     'wS 1; pe >])
+*)
+let explain_type_error k ctx = function
+  | UnboundRel n -> 
+      explain_unbound_rel k ctx n
+  | CantExecute c -> 
+      explain_cant_execute k ctx c
+  | NotAType c -> 
+      explain_not_type k ctx c
+  | BadAssumption c -> 
+      explain_bad_assumption k ctx c
+  | ReferenceVariables id -> 
+      explain_reference_variables id
+  | ElimArity (ind, aritylst, c, p, pt, okinds) ->
+      explain_elim_arity k ctx ind aritylst c p pt okinds 
+  | CaseNotInductive (c, ct) -> 
+      explain_case_not_inductive k ctx c ct
+  | NumberBranches (c, ct, n) -> 
+      explain_number_branches k ctx c ct n
+  | IllFormedBranch (c, i, actty, expty) -> 
+      explain_ill_formed_branch k ctx c i actty expty 
+  | Generalization (nvar, c) ->
+      explain_generalization k ctx nvar c
+  | ActualType (c, ct, pt) -> 
+      explain_actual_type k ctx c ct pt
+  | CantAply (s, rator, randl) ->
+      explain_cant_apply k ctx s rator randl
+  | IllFormedRecBody (i, lna, vdefj, vargs) ->
+      explain_ill_formed_rec_body k ctx i lna vdefj vargs
+  | IllTypedRecBody (i, lna, vdefj, vargs) ->
+      explain_ill_typed_rec_body k ctx i lna vdefj vargs
+  | NotInductive c ->
+      explain_not_inductive k ctx c
+  | MLCase (mes,c,ct,br,brt) ->
+      explain_ml_case k ctx mes c ct br brt
+
+let explain_refiner_bad_type k ctx arg ty conclty =
+  errorlabstrm "Logic.conv_leq_goal"
+    [< 'sTR"refiner was given an argument"; 'bRK(1,1); 
+       P.pr_term k ctx arg; 'sPC;
+       'sTR"of type"; 'bRK(1,1); P.pr_term k ctx ty; 'sPC;
+       'sTR"instead of"; 'bRK(1,1); P.pr_term k ctx conclty >]
+
+let explain_refiner_occur_meta k ctx t =
+  errorlabstrm "Logic.mk_refgoals"
+    [< 'sTR"cannot refine with term"; 'bRK(1,1); P.pr_term k ctx t;
+       'sPC; 'sTR"because there are metavariables, and it is";
+       'sPC; 'sTR"neither an application nor a Case" >]
+
+let explain_refiner_cannot_applt k ctx t harg =
+  errorlabstrm "Logic.mkARGGOALS"
+    [< 'sTR"in refiner, a term of type "; 'bRK(1,1);
+       P.pr_term k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
+       P.pr_term k ctx harg >]
+
+let explain_occur_check k ctx ev rhs =
+  let id = "?" ^ string_of_int ev in
+  let pt = P.pr_term k ctx rhs in
+  errorlabstrm "Trad.occur_check"
+    [< 'sTR"Occur check failed: tried to define "; 'sTR id;
+      'sTR" with term"; 'bRK(1,1); pt >]
+
+let explain_not_clean k ctx sp t =
+  let c = Rel (Intset.choose (free_rels t)) in
+  let id = string_of_id (Names.basename sp) in
+  let var = P.pr_term k ctx c in
+  errorlabstrm "Trad.not_clean"
+    [< 'sTR"Tried to define "; 'sTR id;
+       'sTR" with a term using variable "; var; 'sPC;
+       'sTR"which is not in its scope." >]
+
+end
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
new file mode 100644
index 000000000..ff3eac8ee
--- /dev/null
+++ b/toplevel/fhimsg.mli
@@ -0,0 +1,73 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Names
+open Term
+open Sign
+open Environ
+open Type_errors
+(*i*)
+
+(* This module provides functions to explain the various typing errors.
+   It is parameterized by a function to pretty-print a term in a given
+   context. *)
+
+module type Printer = sig
+  val pr_term : path_kind -> context -> constr -> std_ppcmds
+end
+
+(*s The result is a module which provides a function [explain_type_error]
+  to explain a type error for a given kind in a given context, which are 
+  usually the three arguments carried by the exception [TypeError] 
+  (see \refsec{typeerrors}). *)
+
+module Make (P : Printer) : sig
+
+val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
+
+val pr_ne_ctx : std_ppcmds -> path_kind -> context -> std_ppcmds
+
+val explain_unbound_rel : path_kind -> context -> int -> std_ppcmds
+
+val explain_cant_execute : path_kind -> context -> constr -> std_ppcmds
+
+val explain_not_type : path_kind -> context -> constr -> std_ppcmds
+
+val explain_bad_assumption : path_kind -> context -> constr -> std_ppcmds
+ 
+val explain_reference_variables : identifier -> std_ppcmds
+
+val explain_elim_arity : 
+  path_kind -> context -> constr -> constr list -> constr 
+    -> constr -> constr -> (constr * constr * string) option -> std_ppcmds
+
+val explain_case_not_inductive : 
+  path_kind -> context -> constr -> constr -> std_ppcmds
+
+val explain_number_branches : 
+  path_kind -> context -> constr -> constr -> int -> std_ppcmds
+
+val explain_ill_formed_branch :
+  path_kind -> context -> constr -> int -> constr -> constr -> std_ppcmds
+
+val explain_generalization :
+  path_kind -> context -> name * typed_type -> constr -> std_ppcmds
+
+val explain_actual_type :
+  path_kind -> context -> constr -> constr -> constr -> std_ppcmds
+
+val explain_cant_apply : 
+  path_kind -> context -> string -> unsafe_judgment 
+    -> unsafe_judgment list -> std_ppcmds
+
+val explain_ill_formed_rec_body :
+  path_kind -> context -> std_ppcmds -> 
+    name list -> int -> constr array -> std_ppcmds
+
+val explain_ill_typed_rec_body  :
+  path_kind -> context -> int -> name list -> unsafe_judgment array 
+    -> typed_type array -> std_ppcmds
+
+end
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 419488a37..550105b21 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -3,6 +3,7 @@
 
 open Pp
 open Util
+open Options
 open Names
 open Generic
 open Term
@@ -10,70 +11,28 @@ open Sign
 open Environ
 open Type_errors
 open Reduction
+open Printer
+open Ast
 
-module type Printer = sig
-  val pr_term : path_kind -> context -> constr -> std_ppcmds
-end
-
-module Make = functor (P : Printer) -> struct
-
-  let print_decl k sign (s,typ) =
-    let ptyp = P.pr_term k (gLOB sign) typ.body in 
-    [< 'sPC; print_id s; 'sTR" : "; ptyp >]
-  
-  let print_binding k env = function
-    | Anonymous,ty -> 
-	[< 'sPC; 'sTR"_" ; 'sTR" : " ; P.pr_term k env ty.body >]
-    | Name id,ty -> 
-	[< 'sPC; print_id id ; 'sTR" : "; P.pr_term k env ty.body >]
-
-  let sign_it_with f sign e =
-    snd (sign_it 
-	   (fun id t (sign,e) -> (add_sign (id,t) sign, f id t sign e))
-           sign (nil_sign,e))
-
-  let dbenv_it_with f env e =
-    snd (dbenv_it 
-	   (fun na t (env,e) -> (add_rel (na,t) env, f na t env e))
-           env (gLOB(get_globals env),e))
-      
-  let pr_env k env =
-    let sign_env =
-      sign_it_with
-	(fun id t sign pps ->
-           let pidt =  print_decl k sign (id,t) in [<  pps ; 'fNL ; pidt >])
-	(get_globals env) [< >] 
-    in
-    let db_env =
-      dbenv_it_with 
-	(fun na t env pps ->
-           let pnat = print_binding k env (na,t) in [<  pps ; 'fNL ; pnat >])
-	env [< >]
-    in 
-    [< sign_env; db_env >]
-    
-  let pr_ne_ctx header k = function
-    | ENVIRON (([],[]),[]) -> [< >]
-    | env -> [< header; pr_env k env >]
-
+let guill s = "\""^s^"\""
 
 let explain_unbound_rel k ctx n =
-  let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
+  let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
   [< 'sTR"Unbound reference: "; pe; 'fNL;
      'sTR"The reference "; 'iNT n; 'sTR" is free" >]
 
 let explain_cant_execute k ctx c =
-  let tc = P.pr_term k ctx c in
+  let tc = gentermpr k ctx c in
   [< 'sTR"Cannot execute term:"; 'bRK(1,1); tc >]
 
 let explain_not_type k ctx c =
-  let pe = pr_ne_ctx [< 'sTR"In environment" >] k ctx in
-  let pc = P.pr_term k ctx c in
+  let pe = pr_ne_env [< 'sTR"In environment" >] k ctx in
+  let pc = gentermpr k ctx c in
   [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
      'sTR"should be typed by Set, Prop or Type." >];;
 
 let explain_bad_assumption k ctx c =
-  let pc = P.pr_term k ctx c in
+  let pc = gentermpr k ctx c in
   [< 'sTR "Cannot declare a variable or hypothesis over the term";
      'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];;
 
@@ -83,8 +42,8 @@ let explain_reference_variables id =
 
 let msg_bad_elimination ctx k = function
   | Some(ki,kp,explanation) ->
-      let pki = P.pr_term k ctx ki in
-      let pkp = P.pr_term k ctx kp in
+      let pki = gentermpr k ctx ki in
+      let pkp = gentermpr k ctx kp in
       (hOV 0 
          [< 'fNL; 'sTR "Elimination of an inductive object of sort : ";
             pki; 'bRK(1,0);
@@ -94,11 +53,11 @@ let msg_bad_elimination ctx k = function
       [<>]
 
 let explain_elim_arity k ctx ind aritylst c p pt okinds = 
-  let pi = P.pr_term k ctx ind in
-  let ppar = prlist_with_sep pr_coma (P.pr_term k ctx) aritylst in
-  let pc = P.pr_term k ctx c in
-  let pp = P.pr_term k ctx p in
-  let ppt = P.pr_term k ctx pt in
+  let pi = gentermpr k ctx ind in
+  let ppar = prlist_with_sep pr_coma (gentermpr k ctx) aritylst in
+  let pc = gentermpr k ctx c in
+  let pp = gentermpr k ctx p in
+  let ppt = gentermpr k ctx pt in
   [< 'sTR "Incorrect elimination of"; 'bRK(1,1); pc; 'sPC;
      'sTR "in the inductive type"; 'bRK(1,1); pi; 'fNL;
      'sTR "The elimination predicate"; 'bRK(1,1); pp; 'sPC;
@@ -107,57 +66,57 @@ let explain_elim_arity k ctx ind aritylst c p pt okinds =
      msg_bad_elimination ctx k okinds >]
 
 let explain_case_not_inductive k ctx c ct =
-  let pc = P.pr_term k ctx c in
-  let pct = P.pr_term k ctx ct in
+  let pc = gentermpr k ctx c in
+  let pct = gentermpr k ctx ct in
   [< 'sTR "In Cases expression"; 'bRK(1,1); pc; 'sPC; 
      'sTR "has type"; 'bRK(1,1); pct; 'sPC; 
      'sTR "which is not an inductive definition" >]
   
 let explain_number_branches k ctx c ct expn =
-  let pc = P.pr_term k ctx c in
-  let pct = P.pr_term k ctx ct in
+  let pc = gentermpr k ctx c in
+  let pct = gentermpr k ctx ct in
   [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
      'sTR "of type"; 'bRK(1,1); pct; 'sPC;
      'sTR "expects ";  'iNT expn; 'sTR " branches" >]
 
 let explain_ill_formed_branch k ctx c i actty expty =
-  let pc = P.pr_term k ctx c in
-  let pa = P.pr_term k ctx actty in
-  let pe = P.pr_term k ctx expty in
+  let pc = gentermpr k ctx c in
+  let pa = gentermpr k ctx actty in
+  let pe = gentermpr k ctx expty in
   [< 'sTR "In Cases expression on term"; 'bRK(1,1); pc;
      'sPC; 'sTR "the branch " ; 'iNT (i+1);
      'sTR " has type"; 'bRK(1,1); pa ; 'sPC; 
      'sTR "which should be:"; 'bRK(1,1); pe >]
 
 let explain_generalization k ctx (name,var) c =
-  let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
-  let pv = P.pr_term k ctx var.body in
-  let pc = P.pr_term k (add_rel (name,var) ctx) c in
+  let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
+  let pv = gentermpr k ctx var.body in
+  let pc = gentermpr k (add_rel (name,var) ctx) c in
   [< 'sTR"Illegal generalization: "; pe; 'fNL;
      'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
      'sTR"over"; 'bRK(1,1); pc; 'sPC;
      'sTR"which should be typed by Set, Prop or Type." >]
 
 let explain_actual_type k ctx c ct pt =
-  let pe = pr_ne_ctx [< 'sTR"In environment" >] k ctx in
-  let pc = P.pr_term k ctx c in
-  let pct = P.pr_term k ctx ct in
-  let pt = P.pr_term k ctx pt in
+  let pe = pr_ne_env [< 'sTR"In environment" >] k ctx in
+  let pc = gentermpr k ctx c in
+  let pct = gentermpr k ctx ct in
+  let pt = gentermpr k ctx pt in
   [< pe; 'fNL;
      'sTR"The term"; 'bRK(1,1); pc ; 'sPC ;
      'sTR"does not have type"; 'bRK(1,1); pt; 'fNL;
      'sTR"Actually, it has type" ; 'bRK(1,1); pct >]
 
 let explain_cant_apply k ctx s rator randl =
-  let pe = pr_ne_ctx [< 'sTR"in environment" >] k ctx in
-  let pr = P.pr_term k ctx rator.uj_val in
-  let prt = P.pr_term k ctx rator.uj_type in
+  let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
+  let pr = gentermpr k ctx rator.uj_val in
+  let prt = gentermpr k ctx rator.uj_type in
   let term_string = if List.length randl > 1 then "terms" else "term" in
   let appl = 
     prlist_with_sep pr_fnl
       (fun c ->
-         let pc = P.pr_term k ctx c.uj_val in
-         let pct = P.pr_term k ctx c.uj_type in
+         let pc = gentermpr k ctx c.uj_val in
+         let pct = gentermpr k ctx c.uj_type in
          hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl 
   in
   [< 'sTR"Illegal application ("; 'sTR s; 'sTR"): "; pe; 'fNL;
@@ -168,7 +127,7 @@ let explain_cant_apply k ctx s rator randl =
 
 (* (co)fixpoints *)
 let explain_ill_formed_rec_body k ctx str lna i vdefs =
-  let pvd = P.pr_term k ctx vdefs.(i) in
+  let pvd = gentermpr k ctx vdefs.(i) in
   let s =
     match List.nth lna i with Name id -> string_of_id id | Anonymous -> "_" in
   [< str; 'fNL; 'sTR"The ";
@@ -178,30 +137,30 @@ let explain_ill_formed_rec_body k ctx str lna i vdefs =
      'sTR "is not well-formed" >]
     
 let explain_ill_typed_rec_body k ctx i lna vdefj vargs =
-  let pvd = P.pr_term k ctx (vdefj.(i)).uj_val in
-  let pvdt = P.pr_term k ctx (vdefj.(i)).uj_type in
-  let pv = P.pr_term k ctx (body_of_type vargs.(i)) in
+  let pvd = gentermpr k ctx (vdefj.(i)).uj_val in
+  let pvdt = gentermpr k ctx (vdefj.(i)).uj_type in
+  let pv = gentermpr k ctx (body_of_type vargs.(i)) in
   [< 'sTR"The " ;
      if Array.length vdefj = 1 then [<>] else [<'iNT (i+1); 'sTR "-th">];
      'sTR"recursive definition" ; 'sPC; pvd; 'sPC;
      'sTR "has type"; 'sPC; pvdt;'sPC; 'sTR "it should be"; 'sPC; pv >]
 
 let explain_not_inductive k ctx c =
-  let pc = P.pr_term k ctx c in
+  let pc = gentermpr k ctx c in
   [< 'sTR"The term"; 'bRK(1,1); pc; 'sPC;
      'sTR "is not an inductive definition" >]
 
 let explain_ml_case k ctx mes c ct br brt =
-  let pc = P.pr_term k ctx c in
-  let pct = P.pr_term k ctx ct in
+  let pc = gentermpr k ctx c in
+  let pct = gentermpr k ctx ct in
   let expln =
     match mes with
       | "Inductive" -> [< pct; 'sTR "is not an inductive definition">]
       | "Predicate" -> [< 'sTR "ML case not allowed on a predicate">]
       | "Absurd" -> [< 'sTR "Ill-formed case expression on an empty type" >]
       | "Decomp" ->
-          let plf = P.pr_term k ctx br in
-          let pft = P.pr_term k ctx brt in
+          let plf = gentermpr k ctx br in
+          let pft = gentermpr k ctx brt in
           [< 'sTR "The branch "; plf; 'wS 1; 'cUT; 'sTR "has type "; pft;
              'wS 1; 'cUT;
              'sTR "does not correspond to the inductive definition" >]
@@ -212,14 +171,34 @@ let explain_ml_case k ctx mes c ct br brt =
   hOV 0 [< 'sTR "In ML case expression on "; pc; 'wS 1; 'cUT ;
            'sTR "of type";  'wS 1; pct; 'wS 1; 'cUT; 
            'sTR "which is an inductive predicate."; 'fNL; expln >]
-(*
-let explain_cant_find_case_type loc k ctx c =
-  let pe = P.pr_term k ctx c in
-  Ast.user_err_loc
+
+let explain_cant_find_case_type k ctx c =
+  let pe = gentermpr k ctx c in
+  hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 'wS 1; pe >]
+
+let explain_cant_find_case_type_loc loc k ctx c =
+  let pe = gentermpr k ctx c in
+  user_err_loc
     (loc,"pretype",
      hOV 3 [<'sTR "Cannot infer type of whole Case expression on"; 
 	     'wS 1; pe >])
-*)
+
+let explain_occur_check k ctx ev rhs =
+  let id = "?" ^ string_of_int ev in
+  let pt = gentermpr k ctx rhs in
+  errorlabstrm "Trad.occur_check"
+    [< 'sTR"Occur check failed: tried to define "; 'sTR id;
+      'sTR" with term"; 'bRK(1,1); pt >]
+
+let explain_not_clean k ctx ev t =
+  let c = Rel (Intset.choose (free_rels t)) in
+  let id = "?" ^ string_of_int ev in
+  let var = gentermpr k ctx c in
+  errorlabstrm "Trad.not_clean"
+    [< 'sTR"Tried to define "; 'sTR id;
+       'sTR" with a term using variable "; var; 'sPC;
+       'sTR"which is not in its scope." >]
+
 let explain_type_error k ctx = function
   | UnboundRel n -> 
       explain_unbound_rel k ctx n
@@ -253,40 +232,97 @@ let explain_type_error k ctx = function
       explain_not_inductive k ctx c
   | MLCase (mes,c,ct,br,brt) ->
       explain_ml_case k ctx mes c ct br brt
+  | CantFindCaseType c ->
+      explain_cant_find_case_type k ctx c
+  | OccurCheck (n,c) ->
+      explain_occur_check k ctx n c
+  | NotClean (n,c) ->
+      explain_not_clean k ctx n c
 
 let explain_refiner_bad_type k ctx arg ty conclty =
   errorlabstrm "Logic.conv_leq_goal"
     [< 'sTR"refiner was given an argument"; 'bRK(1,1); 
-       P.pr_term k ctx arg; 'sPC;
-       'sTR"of type"; 'bRK(1,1); P.pr_term k ctx ty; 'sPC;
-       'sTR"instead of"; 'bRK(1,1); P.pr_term k ctx conclty >]
+       gentermpr k ctx arg; 'sPC;
+       'sTR"of type"; 'bRK(1,1); gentermpr k ctx ty; 'sPC;
+       'sTR"instead of"; 'bRK(1,1); gentermpr k ctx conclty >]
 
 let explain_refiner_occur_meta k ctx t =
   errorlabstrm "Logic.mk_refgoals"
-    [< 'sTR"cannot refine with term"; 'bRK(1,1); P.pr_term k ctx t;
+    [< 'sTR"cannot refine with term"; 'bRK(1,1); gentermpr k ctx t;
        'sPC; 'sTR"because there are metavariables, and it is";
        'sPC; 'sTR"neither an application nor a Case" >]
 
 let explain_refiner_cannot_applt k ctx t harg =
   errorlabstrm "Logic.mkARGGOALS"
     [< 'sTR"in refiner, a term of type "; 'bRK(1,1);
-       P.pr_term k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
-       P.pr_term k ctx harg >]
+       gentermpr k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
+       gentermpr k ctx harg >]
 
-let explain_occur_check k ctx ev rhs =
-  let id = "?" ^ string_of_int ev in
-  let pt = P.pr_term k ctx rhs in
-  errorlabstrm "Trad.occur_check"
-    [< 'sTR"Occur check failed: tried to define "; 'sTR id;
-      'sTR" with term"; 'bRK(1,1); pt >]
+let fmt_disclaimer() = 
+  [< 'sTR"If this is in user-written tactic code, then" ; 'sPC ;
+     'sTR"it needs to be modified." ; 'sPC ;
+     'sTR"If this is in system code, then"; 'sPC;
+     'sTR"it needs to be reported." >]
 
-let explain_not_clean k ctx sp t =
-  let c = Rel (Intset.choose (free_rels t)) in
-  let id = string_of_id (Names.basename sp) in
-  let var = P.pr_term k ctx c in
-  errorlabstrm "Trad.not_clean"
-    [< 'sTR"Tried to define "; 'sTR id;
-       'sTR" with a term using variable "; var; 'sPC;
-       'sTR"which is not in its scope." >]
+let print_loc loc =
+  if loc = dummy_loc then 
+    [< 'sTR"<unknown>" >]
+  else 
+    [< 'iNT (fst loc); 'sTR"-"; 'iNT (snd loc) >]
+
+let rec explain_error = function
+  | Stream.Failure -> [< 'sTR"Error: uncaught Parse.Failure." >]
+	
+  | Stream.Error txt -> hOV 0 [< 'sTR"Syntax error: "; 'sTR txt >]
+  | Token.Error txt -> hOV 0 [< 'sTR"Lexer error: "; 'sTR txt >]
+  | Lexer.BadToken tok ->
+      hOV 0 [< 'sTR"Error: the token '"; 'sTR tok;
+               'sTR"' does not respect the lexer rules." >]
+
+  | Sys_error msg -> hOV 0 [< 'sTR"OS error: " ; 'sTR msg >]
+
+  | UserError(s,pps) ->
+      hOV 1 [< 'sTR"Error: ";
+               (if !debug then  [< 'sTR (guill s); 'sTR"."; 'sPC >] else [<>]);
+               pps >]
+
+  | Out_of_memory -> [< 'sTR"Out of memory" >]
+  | Stack_overflow -> [< 'sTR"Stack overflow" >]
+
+  | Anomaly (s,pps) ->
+      hOV 1 [< 'sTR"System Anomaly: ";
+               (if !debug then  [< 'sTR (guill s); 'sTR"."; 'sPC >] else [<>]);
+               pps; 'fNL; fmt_disclaimer() >]
+
+  | Match_failure(filename,pos1,pos2) ->
+      hOV 1 [< 'sTR"Match failure in file " ;
+               'sTR filename ; 'sPC; 'sTR "from char #" ;
+               'iNT pos1 ; 'sTR " to #" ; 'iNT pos2 ; 'sTR ".";
+               'fNL; fmt_disclaimer() >]
+
+  | Ast.No_match s ->
+      hOV 0 [< 'sTR"Ast matching error : "; 'sTR (guill s); 'sTR".";
+               'fNL; fmt_disclaimer() >]
+
+  | Not_found -> hOV 0 [< 'sTR"Search error."; 'fNL; fmt_disclaimer() >]
+
+  | Failure(s) ->
+      hOV 0 [< 'sTR "Somebody raised a Failure exception" ; 'sPC;
+	       'sTR (guill s) ; 'sTR "." ; 'fNL; fmt_disclaimer() >]
+
+  | Invalid_argument(s) ->
+      hOV 0 [< 'sTR"Invalid argument: " ; 'sTR (guill s) ; 'sTR "." ;
+               'fNL; fmt_disclaimer() >]
 
-end
+  | Sys.Break -> [<'fNL;  'sTR"User Interrupt." >]
+	
+  | Stdpp.Exc_located (loc,exc) ->
+      hOV 0 [< if loc = Ast.dummy_loc then [<>]
+               else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
+               explain_error exc >]
+	
+  | reraise ->
+      flush_all();
+      (try Printexc.print raise reraise with _ -> ());
+      flush_all();
+      fmt_disclaimer()
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index ff3eac8ee..3a576b511 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -10,64 +10,9 @@ open Environ
 open Type_errors
 (*i*)
 
-(* This module provides functions to explain the various typing errors.
-   It is parameterized by a function to pretty-print a term in a given
-   context. *)
-
-module type Printer = sig
-  val pr_term : path_kind -> context -> constr -> std_ppcmds
-end
-
-(*s The result is a module which provides a function [explain_type_error]
-  to explain a type error for a given kind in a given context, which are 
-  usually the three arguments carried by the exception [TypeError] 
-  (see \refsec{typeerrors}). *)
-
-module Make (P : Printer) : sig
+(* This module provides functions to explain the various errors. *)
 
 val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
 
-val pr_ne_ctx : std_ppcmds -> path_kind -> context -> std_ppcmds
-
-val explain_unbound_rel : path_kind -> context -> int -> std_ppcmds
-
-val explain_cant_execute : path_kind -> context -> constr -> std_ppcmds
-
-val explain_not_type : path_kind -> context -> constr -> std_ppcmds
-
-val explain_bad_assumption : path_kind -> context -> constr -> std_ppcmds
- 
-val explain_reference_variables : identifier -> std_ppcmds
-
-val explain_elim_arity : 
-  path_kind -> context -> constr -> constr list -> constr 
-    -> constr -> constr -> (constr * constr * string) option -> std_ppcmds
-
-val explain_case_not_inductive : 
-  path_kind -> context -> constr -> constr -> std_ppcmds
-
-val explain_number_branches : 
-  path_kind -> context -> constr -> constr -> int -> std_ppcmds
-
-val explain_ill_formed_branch :
-  path_kind -> context -> constr -> int -> constr -> constr -> std_ppcmds
-
-val explain_generalization :
-  path_kind -> context -> name * typed_type -> constr -> std_ppcmds
-
-val explain_actual_type :
-  path_kind -> context -> constr -> constr -> constr -> std_ppcmds
-
-val explain_cant_apply : 
-  path_kind -> context -> string -> unsafe_judgment 
-    -> unsafe_judgment list -> std_ppcmds
-
-val explain_ill_formed_rec_body :
-  path_kind -> context -> std_ppcmds -> 
-    name list -> int -> constr array -> std_ppcmds
-
-val explain_ill_typed_rec_body  :
-  path_kind -> context -> int -> name list -> unsafe_judgment array 
-    -> typed_type array -> std_ppcmds
+val explain_error : exn -> std_ppcmds
 
-end
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 9d2d5ec92..a5e421fed 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -110,7 +110,7 @@ let parse_file f =
     | End_of_file | Stdpp.Exc_located (_, End_of_file) -> close_in c; exit 0
     | exn -> close_in c; raise exn
 
-module Explain = Himsg.Make(struct let pr_term = pr_term end)
+module Explain = Fhimsg.Make(struct let pr_term = pr_term end)
 
 let rec explain_exn = function
   | TypeError (k,ctx,te) -> 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
new file mode 100644
index 000000000..2c230365d
--- /dev/null
+++ b/toplevel/usage.ml
@@ -0,0 +1,54 @@
+
+(* $Id$ *)
+
+(* print the usage of coqtop (or coqc) on channel co *)
+
+let print_usage_channel co command =
+  output_string co command;
+  output_string co "Options are:\n";
+  output_string co
+"  -I dir                 add directory dir in the include path
+  -include dir           (idem)
+  -R dir                 add recursively dir
+  -src                   add source directories in the include path
+
+  -inputstate f          read state from file f.coq
+  -is f                  (idem)
+  -nois                  start with an empty state
+  -outputstate f         write state in file f.coq
+
+  -load-ml-object f      load ML object file f 
+  -load-ml-source f      load ML file f 
+  -load-vernac-source f  load Coq file f.v (Load f.)
+  -load-vernac-object f  load Coq object file f.vo
+  -require f             load Coq object file f.vo and import it (Require f.)
+
+  -opt                   run the native-code version of Coq or Coq_SearchIsos
+  -full                  run the native-code version of Coq with all tactics
+  -image f               specify an alternative binary image f
+  -bindir dir            specify an alternative directory for the binaries
+  -libdir dir            specify an alternative directory for the library
+
+  -where                 print Coq's standard library location and exit
+  -v                     print Coq version and exit
+
+  -q                     skip loading of rcfile
+  -init-file f           give the rcfile f
+  -user u                give the user u
+  -batch                 batch mode (exits just after arguments parsing)
+  -emacs                 tells Coq it is executed under Emacs
+"
+
+(* print the usage on standard error *)
+
+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";;
+
+let print_usage_coqc () =
+  print_usage "Usage: coqc [-i] [-t] <options> file...\n
+  -i  compile specification only (in file.vi)
+  -t  keep temporary files\n\n"
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
new file mode 100644
index 000000000..0cd71ad09
--- /dev/null
+++ b/toplevel/usage.mli
@@ -0,0 +1,7 @@
+
+(* $Id$ *)
+
+(* Prints the usage on the error output. *)
+
+val print_usage_coqtop : unit -> unit
+val print_usage_coqc : unit -> unit
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 65bb4f4d8..f6f696ea3 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -90,23 +90,34 @@ let just_parsing = ref false
 
 let rec vernac interpfun input =
   let com = parse_phrase input in
-  try
-    match com with
-      | Node (_,"LoadFile",[Str(_, verbosely); Str(_,fname)]) ->
-          let verbosely = verbosely = "Verbose" in
-          raw_load_vernac_file verbosely (make_suffix fname ".v")
-            
-      | Node (_,"CompileFile",[Str(_,verbosely); Str(_,only_spec);
-                               Str (_,mname); Str(_,fname)]) ->
-          let verbosely = verbosely = "Verbose" in
-          let only_spec = only_spec = "Specification" in
-          States.with_heavy_rollback (* to roll back in case of error *)
-            (raw_compile_module verbosely only_spec mname)
-            (make_suffix fname ".v")
-      | _ -> if not !just_parsing then interpfun com
-  with e -> 
-    raise (DuringCommandInterp (Ast.loc com, e))
-      
+  let rec interp com =
+    try
+      match com with
+	| Node (_,"LoadFile",[Str(_, verbosely); Str(_,fname)]) ->
+            let verbosely = verbosely = "Verbose" in
+            raw_load_vernac_file verbosely (make_suffix fname ".v")
+              
+	| Node (_,"CompileFile",[Str(_,verbosely); Str(_,only_spec);
+				 Str (_,mname); Str(_,fname)]) ->
+            let verbosely = verbosely = "Verbose" in
+            let only_spec = only_spec = "Specification" in
+            States.with_heavy_rollback (* to roll back in case of error *)
+              (raw_compile_module verbosely only_spec mname)
+              (make_suffix fname ".v")
+	      
+	| Node(_,"Time",l) ->
+	    let tstart = System.get_time() in
+            List.iter interp l;
+	    let tend = System.get_time() in
+            mSGNL [< 'sTR"Finished transaction in " ;
+                     System.fmt_time_difference tstart tend >]
+	      
+	| _ -> if not !just_parsing then interpfun com
+    with e -> 
+      raise (DuringCommandInterp (Ast.loc com, e))
+  in 
+  interp com
+     
 and raw_load_vernac_file verbosely s =
   let _ = read_vernac_file verbosely s in ()
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b19bcabb5..8989460c0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1390,6 +1390,66 @@ let _ =
 		  mSG(print_name t))
      | _ -> bad_vernac_args "TableField")
 
+
+open Tactics
+open Pfedit
+
+(* 
+   The first one is a command that should be a tactic. It has been
+   added by Christine to patch an error in the design of the proof
+   machine, and enables to instantiate existential variables when
+   there are no more goals to solve. It cannot be a tactic since 
+   all tactics fail if there are no further goals to prove. *)
+
+let _ = 
+  vinterp_add "EXISTENTIAL"
+    (function 
+       | [VARG_NUMBER n; VARG_COMMAND c] -> 
+           (fun () -> mutate (instantiate_pf_com n c))
+       |  _  -> assert false)
+
+(* The second is a stupid macro that should be replaced by ``Exact
+   c. Save.'' all along the theories. *)
+
+let _ = 
+  vinterp_add "PROOF"
+    (function 
+       | [VARG_COMMAND c] ->
+           (fun () -> (* by (tactic_com exact c) *)
+              (* on experimente la synthese d'ise dans exact *)
+              by (dyn_exact [Command c]); 
+              save_named true)
+       |   _  -> assert false)
+
+let print_subgoals () = 
+  if not (is_silent()) then show_open_subgoals_focused()
+
+let _ = 
+  vinterp_add "SOLVE"
+    (function l -> 
+       let (n,tcom) = match l with 
+	 | [VARG_NUMBER n;VARG_TACTIC tcom] -> (n,tcom)
+	 |  _  -> invalid_arg "SOLVE"
+       in
+       (fun () -> 
+	  (match Tacinterp.is_just_undef_macro tcom with
+             | Some id -> 
+		 let msg =
+ 	     	   if Pfedit.refining () then 
+		     "undefined command or tactic"
+	     	   else 
+		     "undefined command"
+		 in 
+		 error msg
+	     | None -> ());
+	  solve_nth n (Tacinterp.vernac_interp tcom);
+	  print_subgoals();
+          (* in case a strict subtree was completed, 
+              go back to the top of the prooftree *) 
+	  if subtree_solved () then 
+	    (rev_mutate top_of_tree; print_subgoals()) 
+       ))
+
 (*Only for debug*)
 (***
 let _ =
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 9b7e62b23..412575a03 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -119,14 +119,7 @@ let call (opn,converted_args) =
 	  mSGNL [< 'sTR"Vernac Interpreter " ; 'sTR !loc >];
         raise e
 
-let rec interp = function
-  (*** now done in vernac.ml
-  | Node(_,"Time",l) -> 
-      let tstart = System.timestamp() in
-      List.iter interp l;
-      mSGNL [< 'sTR"Finished transaction in " ;
-               System.fmt_time_difference tstart (System.timestamp()) >]
-  ***)
+let interp = function
   | Node(_,opn,argl) as cmd ->
       let converted_args =
       	try