- coqmktop

 - #use "include.ml";;


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

10 files changed, 156 insertions, 150 deletions

diff --git a/.depend b/.depend
index 17ae5aaf8..978f5368c 100644
--- a/.depend
+++ b/.depend
@@ -140,10 +140,10 @@ tactics/tacentries.cmi: proofs/proof_trees.cmi proofs/tacmach.cmi
 tactics/tacticals.cmi: proofs/clenv.cmi kernel/names.cmi tactics/pattern.cmi \
     proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \
     proofs/tacmach.cmi kernel/term.cmi tactics/wcclausenv.cmi 
-tactics/tactics.cmi: proofs/clenv.cmi kernel/environ.cmi kernel/evd.cmi \
-    kernel/names.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
-    proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \
-    kernel/term.cmi 
+tactics/tactics.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/environ.cmi \
+    kernel/evd.cmi kernel/names.cmi proofs/proof_trees.cmi \
+    kernel/reduction.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
+    tactics/tacticals.cmi kernel/term.cmi 
 tactics/termdn.cmi: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi 
 tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \
     proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
@@ -310,8 +310,10 @@ library/declare.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
     library/libobject.cmx kernel/names.cmx library/nametab.cmx \
     kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \
     kernel/univ.cmx lib/util.cmx library/declare.cmi 
-library/discharge.cmo: library/declare.cmi library/discharge.cmi 
-library/discharge.cmx: library/declare.cmx library/discharge.cmi 
+library/discharge.cmo: library/declare.cmi library/lib.cmi \
+    library/discharge.cmi 
+library/discharge.cmx: library/declare.cmx library/lib.cmx \
+    library/discharge.cmi 
 library/global.cmo: kernel/environ.cmi kernel/generic.cmi \
     kernel/inductive.cmi kernel/instantiate.cmi kernel/safe_typing.cmi \
     kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
@@ -620,6 +622,8 @@ proofs/tacmach.cmx: parsing/ast.cmx parsing/astterm.cmx library/declare.cmx \
     kernel/reduction.cmx proofs/refiner.cmx kernel/sign.cmx lib/stamps.cmx \
     pretyping/tacred.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \
     proofs/tacmach.cmi 
+scripts/coqmktop.cmo: config/coq_config.cmi scripts/tolink.cmo 
+scripts/coqmktop.cmx: config/coq_config.cmx scripts/tolink.cmx 
 tactics/auto.cmo: tactics/btermdn.cmi proofs/clenv.cmi library/declare.cmi \
     tactics/dhyp.cmi kernel/evd.cmi kernel/generic.cmi library/global.cmi \
     tactics/hiddentac.cmi kernel/inductive.cmi library/lib.cmi \
@@ -765,19 +769,19 @@ 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/errors.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/errors.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 toplevel/himsg.cmi lib/options.cmi \
+    lib/pp.cmi kernel/type_errors.cmi lib/util.cmi toplevel/errors.cmi 
+toplevel/errors.cmx: parsing/ast.cmx toplevel/himsg.cmx lib/options.cmx \
+    lib/pp.cmx kernel/type_errors.cmx lib/util.cmx toplevel/errors.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/fhimsg.cmi 
@@ -785,12 +789,12 @@ 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/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/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 \
@@ -848,27 +852,29 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
     toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.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 \
-    pretyping/tacred.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
+    library/declare.cmi library/discharge.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/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
+    tactics/tactics.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/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 \
-    pretyping/tacred.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
+    library/declare.cmx library/discharge.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/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
+    tactics/tactics.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 \
diff --git a/Makefile b/Makefile
index a492fd0c6..8db9dc19e 100644
--- a/Makefile
+++ b/Makefile
@@ -1,16 +1,33 @@
-# Main Makefile for Coq
+
+###########################################################################
+# Makefile for Coq
+#
+# This is the only Makefile. You won't find Makefiles in sub-directories
+# and this is done on purpose. If you are not yet convinced of the advantages
+# of a single Makefile, please read
+#    http://www.pcug.org.au/~millerp/rmch/recu-make-cons-harm.html
+# before complaining.
+# 
+# When you are working in a subdir, you can compile without moving to the
+# upper directory using "make -C ..", and the output is still understood
+# by Emacs' next-error.
+###########################################################################
 
 include config/Makefile
 
 noargument:
-	@echo Please use either
+	@echo "Please use either"
 	@echo "   ./configure"
 	@echo "   make world"
 	@echo "   make install"
 	@echo "   make cleanall"
-	@echo or make archclean
+	@echo "or make archclean"
+
+###########################################################################
+# Compilation options
+###########################################################################
 
-LOCALINCLUDES=-I config -I lib -I kernel -I library \
+LOCALINCLUDES=-I config -I scripts -I lib -I kernel -I library \
               -I proofs -I tactics -I pretyping -I parsing -I toplevel
 INCLUDES=$(LOCALINCLUDES) -I $(CAMLP4LIB)
 
@@ -23,7 +40,11 @@ CAMLP4EXTEND=camlp4o $(INCLUDES) pa_extend.cmo
 OCAMLC_P4O=$(OCAMLC) -pp camlp4o $(BYTEFLAGS)
 OCAMLOPT_P4O=$(OCAMLOPT) -pp camlp4o $(OPTFLAGS)
 
+###########################################################################
 # Objects files 
+###########################################################################
+
+STRLIB=-cclib -lstr
 
 CLIBS=unix.cma
 
@@ -47,7 +68,8 @@ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \
 LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \
 	library/global.cmo library/states.cmo library/library.cmo \
 	library/nametab.cmo library/impargs.cmo library/redinfo.cmo \
-        library/indrec.cmo library/declare.cmo library/goptions.cmo
+        library/indrec.cmo library/declare.cmo library/discharge.cmo \
+        library/goptions.cmo
 
 PRETYPING=pretyping/tacred.cmo pretyping/pretype_errors.cmo \
           pretyping/retyping.cmo pretyping/typing.cmo \
@@ -87,15 +109,40 @@ CMO=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \
     $(PROOFS) $(TACTICS) $(TOPLEVEL)
 CMX=$(CMO:.cmo=.cmx)
 
-# Targets
+###########################################################################
+# Main targets
+###########################################################################
+
+COQMKTOP=scripts/coqmktop
 
 world: minicoq coqtop.byte dev/db_printers.cmo
 
-LINK=$(CONFIG) $(LIB) $(KERNEL) $(LIBRARY) $(PRETYPING) $(PARSING) \
-     $(PROOFS) $(TACTICS) $(TOPLEVEL)
-link: $(LINK)
-	ocamlc -custom $(INCLUDES) -o link dynlink.cma $(CMA) $(LINK) $(OSDEPLIBS)
-	rm -f link 
+coqtop: $(COQMKTOP) $(CMX)
+	$(COQMKTOP) -opt -notactics $(OPTFLAGS) -o coqtop
+
+coqtop.byte: $(COQMKTOP) $(CMO) Makefile
+	$(COQMKTOP) -top -notactics $(BYTEFLAGS) -o coqtop.byte
+
+# coqmktop 
+
+COQMKTOPCMO=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo 
+
+$(COQMKTOP): $(COQMKTOPCMO)
+	$(OCAMLC) $(BYTEFLAGS) -o $(COQMKTOP) -custom str.cma unix.cma $(COQMKTOPCMO) $(OSDEPLIBS) $(STRLIB)
+
+scripts/tolink.ml: Makefile
+	echo "let lib = \""$(LIB)"\"" > $@
+	echo "let kernel = \""$(KERNEL)"\"" >> $@
+	echo "let library = \""$(LIBRARY)"\"" >> $@
+	echo "let pretyping = \""$(PRETYPING)"\"" >> $@
+	echo "let parsing = \""$(PARSING)"\"" >> $@
+	echo "let proofs = \""$(PROOFS)"\"" >> $@
+	echo "let tactics = \""$(TACTICS)"\"" >> $@
+	echo "let toplevel = \""$(TOPLEVEL)"\"" >> $@
+
+beforedepend:: scripts/tolink.ml
+
+# we provide targets for each subdirectories
 
 lib: $(LIB)
 kernel: $(KERNEL)
@@ -106,16 +153,9 @@ parsing: $(PARSING)
 pretyping: $(PRETYPING)
 toplevel: $(TOPLEVEL)
 
-# coqtop
-
-coqtop: $(CMX)
-	$(OCAMLOPT) $(INCLUDES) -o coqtop $(CMXA) $(CMX) $(OSDEPLIBS)
-
-coqtop.byte: $(CMO) Makefile
-	ocamlmktop $(BYTEFLAGS) -o coqtop.byte -custom dynlink.cma $(CMA) \
-	  $(CMO) $(OSDEPLIBS)
-
+###########################################################################
 # minicoq
+###########################################################################
 
 MINICOQCMO=$(CONFIG) $(LIB) $(KERNEL) \
 	   parsing/lexer.cmo parsing/g_minicoq.cmo \
@@ -125,15 +165,16 @@ minicoq: $(MINICOQCMO)
 	$(OCAMLC) $(INCLUDES) -o minicoq -custom $(CMA) $(MINICOQCMO) \
 	  $(OSDEPLIBS)
 
+###########################################################################
 # Documentation
+# Literate programming (with ocamlweb)
+###########################################################################
 
 .PHONY: doc
 
 doc: doc/coq.tex
 	make -C doc coq.ps minicoq.dvi
 
-# Literate programming (with ocamlweb)
-
 LPLIB = lib/doc.tex $(LIB:.cmo=.mli)
 LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
 LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli)
@@ -150,7 +191,9 @@ doc/coq.tex: doc/preamble.tex $(LPFILES)
 	ocamlweb --no-preamble $(LPFILES) >> doc/coq.tex
 	echo "\end{document}" >> doc/coq.tex
 
+###########################################################################
 # Emacs tags
+###########################################################################
 
 tags:
 	find . -name "*.ml*" | sort -r | xargs \
@@ -162,7 +205,9 @@ tags:
 	      "--regex=/val[ \t]+\([^ \t]+\)/\1/" \
 	      "--regex=/module[ \t]+\([^ \t]+\)/\1/"
 
+###########################################################################
 ### Special rules
+###########################################################################
 
 # lexer (compiled with camlp4 to get optimized streams)
 
@@ -210,7 +255,9 @@ parsing/extend.cmx: parsing/extend.ml4 parsing/grammar.cma
 
 beforedepend:: $(GRAMMARCMO)
 
+###########################################################################
 # Default rules
+###########################################################################
 
 .SUFFIXES: .ml .mli .cmo .cmi .cmx .mll .ml4
 
@@ -232,7 +279,9 @@ beforedepend:: $(GRAMMARCMO)
 .ml4.cmx:
 	$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4EXTEND) -impl" -c -impl $<
 
+###########################################################################
 # Cleaning
+###########################################################################
 
 archclean::
 	rm -f config/*.cmx config/*.[so]
@@ -261,7 +310,9 @@ cleanall:: archclean
 cleanconfig::
 	rm -f config/Makefile config/coq_config.ml
 
+###########################################################################
 # Dependencies
+###########################################################################
 
 alldepend: depend dependcamlp4
 
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5f6af5a8b..0131df8b9 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -1050,3 +1050,22 @@ let elim_res_pf kONT clenv gls =
 let e_res_pf kONT clenv gls =
   clenv_refine kONT
     (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
+
+open Printer
+
+let pr_clenv clenv =
+  let pr_name mv =
+    try 
+      let id = Intmap.find mv clenv.namenv in
+      [< 'sTR"[" ; print_id id ; 'sTR"]" >]
+    with Not_found -> [< >]
+  in
+  let pr_meta_binding = function
+    | (mv,Cltyp b) ->
+      	hOV 0 [< 'iNT mv ; pr_name mv ; 'sTR " : " ; prterm b.rebus ; 'fNL >]
+    | (mv,Clval(b,_)) ->
+      	hOV 0 [< 'iNT mv ; pr_name mv ; 'sTR " := " ; prterm b.rebus ; 'fNL >]
+  in
+  [< 'sTR"TEMPL: " ; prterm clenv.templval.rebus ;
+     'sTR" : " ; prterm clenv.templtyp.rebus ; 'fNL ;
+     (prlist pr_meta_binding (intmap_to_list clenv.env)) >]
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f5daf8b36..1f28a73af 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -92,3 +92,6 @@ val clenv_constrain_dep_args_of :
 val constrain_clenv_using_subterm_list : 
   bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list
 val clenv_typed_unify : constr -> constr -> wc clausenv -> wc clausenv
+
+val pr_clenv : 'a clausenv -> Pp.std_ppcmds
+
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a056ca8fc..ecbd1a91c 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -131,9 +131,9 @@ let parse_args () =
 	try
 	  Stream.empty s; exit 1
 	with Stream.Failure ->
-	  mSGNL (Himsg.explain_error e); exit 1
+	  mSGNL (Errors.explain_exn e); exit 1
       end
-    | e -> begin mSGNL (Himsg.explain_error e); exit 1 end
+    | e -> begin mSGNL (Errors.explain_exn e); exit 1 end
 
 
 (* To prevent from doing the initialization twice *)
@@ -163,4 +163,4 @@ let start () =
   if !batch_mode then (flush_all(); Profile.print_profile ();exit 0);
   Toplevel.loop()
 
-let _ = start()
+(* Coqtop.start will be called by the code produced by coqmktop *)
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index 1de6348ec..4029437bf 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -4,6 +4,7 @@
 open Pp
 open Util
 open Ast
+open Type_errors
 
 let print_loc loc =
   if loc = dummy_loc then 
@@ -45,6 +46,8 @@ 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
+
   | Stdpp.Exc_located (loc,exc) ->
       hOV 0 [< if loc = Ast.dummy_loc then [<>]
                else [< 'sTR"At location "; print_loc loc; 'sTR":"; 'fNL >];
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 550105b21..c47c0abc4 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -257,72 +257,3 @@ let explain_refiner_cannot_applt k ctx t harg =
     [< 'sTR"in refiner, a term of type "; 'bRK(1,1);
        gentermpr k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
        gentermpr k ctx harg >]
-
-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 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() >]
-
-  | 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 3a576b511..ea4c10637 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -10,9 +10,6 @@ open Environ
 open Type_errors
 (*i*)
 
-(* This module provides functions to explain the various errors. *)
+(* This module provides functions to explain the type errors. *)
 
 val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
-
-val explain_error : exn -> std_ppcmds
-
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 643433e0c..e78a4b92a 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -102,7 +102,7 @@ let print_highlight_location ib (bp,ep) =
   let highlight_lines =
     match get_bols_of_loc ib (bp,ep) with
       | ([],(bl,el)) ->  
-	  [< 'sTR"> "; 'sTR(String.sub ib.str bl (el-bl));
+	  [< 'sTR"> "; 'sTR(String.sub ib.str bl (el-bl)); 'fNL;
              'sTR"> "; 'sTR(String.make (bp-bl) ' ');
              'sTR(String.make (ep-bp) '^') >]
       | ((b1,e1)::ml,(bn,en)) ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8989460c0..a01e701bc 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -109,20 +109,20 @@ let reset_top_of_tree () =
  
 let locate_file f =
   try
-    mSG [< 'sTR (System.where_in_path (System.search_paths()) f) ; 'fNL >]
+    mSG [< 'sTR (System.where_in_path (System.search_paths()) f); 'fNL >]
   with Not_found -> 
-    mSG [< 'sTR"Can't find file" ; 'sPC ; 'sTR f ; 'sPC ;
-           'sTR"on loadpath" ; 'fNL >]
+    mSG (hOV 0 [< 'sTR"Can't find file"; 'sPC; 'sTR f; 'sPC;
+		  'sTR"on loadpath"; 'fNL >])
 
 let locate_id id =
   try
-    mSG [< 'sTR (string_of_path (Nametab.sp_of_id CCI id)) ; 'fNL >]
+    mSG [< 'sTR (string_of_path (Nametab.sp_of_id CCI id)); 'fNL >]
   with Not_found -> 
     error ((string_of_id id) ^ " not a defined object")
 
 let print_loadpath () =
   let l = search_paths () in
-  mSGNL [< 'sTR"Load Path:" ; 'fNL; 'sTR"  ";
+  mSGNL [< 'sTR"Load Path:"; 'fNL; 'sTR"  ";
            hV 0 (prlist_with_sep pr_fnl (fun s -> [< 'sTR s >]) l) >]
 
 let goal_of_args = function
@@ -304,7 +304,6 @@ let _ =
 	   (fun () -> let _ = Lib.open_section (string_of_id id) in ())
        | _ -> bad_vernac_args "BeginSection")
 
-(***
 let _ =
   add "EndSection"
     (function 
@@ -314,9 +313,8 @@ let _ =
 		errorlabstrm "vernacentries : EndSection"
 		  [< 'sTR"proof editing in progress" ; (msg_proofs false) ;
                      'sTR"Use \"Abort All\" first or complete proof(s)." >];
-              close_section_or_module (not (is_silent())) (string_of_id id))
+              Discharge.close_section (not (is_silent())) (string_of_id id))
        | _ -> bad_vernac_args "EndSection")
-***)
 
 (* Proof switching *)
 
@@ -1110,7 +1108,6 @@ let _ =
        | [] -> (fun () -> ())
        | _  -> bad_vernac_args "NOP")
 
-(***
 let _ =
   add "CLASS"
     (function 
@@ -1140,10 +1137,9 @@ let _ =
 	   in
 	   let isid = identity = "IDENTITY" in
 	   fun () -> 
-	     Class.try_add_new_coercion id stre ids idt isid;
+	     Class.try_add_new_coercion_with_target id stre ids idt isid;
              message ((string_of_id id) ^ " is now a coercion")
        | _ -> bad_vernac_args "COERCION")
-     ***)
 
 let _ =
   add "PrintGRAPH"