affichage des erreurs de typage dans minicoq

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

10 files changed, 147 insertions, 98 deletions

diff --git a/.depend b/.depend
index 712ab7954..630144ee2 100644
--- a/.depend
+++ b/.depend
@@ -187,15 +187,15 @@ toplevel/himsg.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/himsg.cmi 
 toplevel/minicoq.cmo: kernel/constant.cmi parsing/g_minicoq.cmi \
-    kernel/generic.cmi /usr/local/lib/camlp4/grammar.cmi kernel/inductive.cmi \
-    kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
-    /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmi kernel/typing.cmi \
-    lib/util.cmi 
+    kernel/generic.cmi /usr/local/lib/camlp4/grammar.cmi toplevel/himsg.cmi \
+    kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \
+    /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmi kernel/type_errors.cmi \
+    kernel/typing.cmi lib/util.cmi 
 toplevel/minicoq.cmx: kernel/constant.cmx parsing/g_minicoq.cmi \
-    kernel/generic.cmx /usr/local/lib/camlp4/grammar.cmi kernel/inductive.cmx \
-    kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
-    /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmx kernel/typing.cmx \
-    lib/util.cmx 
+    kernel/generic.cmx /usr/local/lib/camlp4/grammar.cmi toplevel/himsg.cmx \
+    kernel/inductive.cmx kernel/names.cmx lib/pp.cmx kernel/sign.cmx \
+    /usr/local/lib/camlp4/stdpp.cmi kernel/term.cmx kernel/type_errors.cmx \
+    kernel/typing.cmx lib/util.cmx 
 parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
     /usr/local/lib/camlp4/gramext.cmi parsing/pcoq.cmi 
 parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx \
diff --git a/Makefile b/Makefile
index d1fd60f35..6ee0156d8 100644
--- a/Makefile
+++ b/Makefile
@@ -10,7 +10,8 @@ noargument:
 	@echo "   make cleanall"
 	@echo or make archclean
 
-INCLUDES=-I config -I lib -I kernel -I library -I parsing -I $(CAMLP4LIB)
+INCLUDES=-I config -I lib -I kernel -I library -I parsing -I toplevel \
+	 -I $(CAMLP4LIB)
 
 BYTEFLAGS=$(INCLUDES) $(CAMLDEBUG)
 OPTFLAGS=$(INCLUDES) $(CAMLTIMEPROF)
@@ -71,7 +72,8 @@ coqtop.byte: $(CMO)
 # minicoq
 
 MINICOQCMO=$(CONFIG) $(LIB) $(KERNEL) \
-	   parsing/lexer.cmo parsing/g_minicoq.cmo toplevel/minicoq.cmo
+	   parsing/lexer.cmo parsing/g_minicoq.cmo \
+	   toplevel/himsg.cmo toplevel/minicoq.cmo
 
 minicoq: $(MINICOQCMO)
 	$(OCAMLC) $(INCLUDES) -o minicoq -custom $(CMA) $(MINICOQCMO) \
@@ -89,7 +91,9 @@ doc: doc/coq.tex
 LPLIB = lib/doc.tex $(LIB:.cmo=.mli)
 LPKERNEL = kernel/doc.tex $(KERNEL:.cmo=.mli)
 LPLIBRARY = library/doc.tex $(LIBRARY:.cmo=.mli)
-LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY)
+LPTOPLEVEL = toplevel/doc.tex $(TOPLEVEL:.cmo=.mli)
+LPFILES = doc/macros.tex doc/intro.tex $(LPLIB) $(LPKERNEL) $(LPLIBRARY) \
+	  $(LPTOPLEVEL)
 
 doc/coq.tex: $(LPFILES)
 	ocamlweb -o doc/coq.tex $(LPFILES)
diff --git a/doc/macros.tex b/doc/macros.tex
index 5a4a2e74d..cfed9a713 100644
--- a/doc/macros.tex
+++ b/doc/macros.tex
@@ -3,3 +3,5 @@
 
 \newcommand{\Coq}{\textsf{Coq}}
 \newcommand{\CCI}{Calculus of Inductive Constructions}
+
+\newcommand{\citesec}[1]{\textbf{\ref{#1}}}
\ No newline at end of file
diff --git a/kernel/term.mli b/kernel/term.mli
index 6ef98691f..7c1ee1d33 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -45,7 +45,7 @@ val mk_Prop : sorts
 
 (*s The type [constr] of the terms of CCI
   is obtained by instanciating the generic terms (type [term], 
-  see \ref{generic_terms}) on the above operators, themselves instanciated
+  see \citesec{generic_terms}) on the above operators, themselves instanciated
   on the above sorts. *)
 
 type constr = sorts oper term
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 3a3e1488e..6632c172f 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -9,7 +9,7 @@ open Sign
 open Environ
 (*i*)
 
-(* Type errors. *)
+(* Type errors. \label{typeerrors} *)
 
 type type_error =
   | UnboundRel of int
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index 1e5b610c6..ae26e3f3c 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -7,6 +7,7 @@ open Names
 open Univ
 open Generic
 open Term
+open Sign
 
 let lexer = {
   Token.func = Lexer.func;
@@ -170,4 +171,4 @@ let rec pp bv = function
   | Rel n -> print_rel bv n
   | _ -> [< 'sTR"<???>" >]
 
-let pr_term = pp []
+let pr_term _ ctx = pp (List.map fst (get_rels ctx))
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
index 77dbb5c71..289706fdb 100644
--- a/parsing/g_minicoq.mli
+++ b/parsing/g_minicoq.mli
@@ -2,6 +2,7 @@
 open Pp
 open Names
 open Term
+open Sign
 
 val term : constr Grammar.Entry.e
 
@@ -16,4 +17,4 @@ type command =
 
 val command : command Grammar.Entry.e
 
-val pr_term : constr -> std_ppcmds
+val pr_term : path_kind -> context -> constr -> std_ppcmds
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 220297d7f..6ed2851e3 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -13,39 +13,73 @@ open Reduction
 
 module type Printer = sig
   val pr_term : path_kind -> context -> constr -> std_ppcmds
-  val pr_ne_ctx : std_ppcmds -> path_kind -> context -> 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 = P.pr_ne_ctx [< 'sTR"in environment" >] k ctx in
-  errorlabstrm "unbound rel"
-    [< 'sTR"Unbound reference: "; pe; 'fNL;
-       'sTR"The reference "; 'iNT n; 'sTR" is free" >]
+  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
-  errorlabstrm "Cannot execute"
-    [< 'sTR"Cannot execute term:"; 'bRK(1,1); tc >]
+  [< 'sTR"Cannot execute term:"; 'bRK(1,1); tc >]
 
 let explain_not_type k ctx c =
-  let pe = P.pr_ne_ctx [< 'sTR"In environment" >] k ctx in
+  let pe = pr_ne_ctx [< 'sTR"In environment" >] k ctx in
   let pc = P.pr_term k ctx c in
-  errorlabstrm "Not a type"
-    [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
-       'sTR"should be typed by Set, Prop or Type." >];;
+  [< 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
-  errorlabstrm "Bad assumption"
-    [< 'sTR "Cannot declare a variable or hypothesis over the term";
-       'bRK(1,1); pc; 'sPC; 'sTR "because this term is not a type." >];;
+  [< '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 =
-  errorlabstrm "construct_reference" 
-    [< 'sTR "the constant"; 'sPC; print_id id; 'sPC; 
-       'sTR "refers to variables which are not in the context" >]
+  [< '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) ->
@@ -56,7 +90,8 @@ let msg_bad_elimination ctx k = function
             pki; 'bRK(1,0);
             'sTR "is not allowed on a predicate in sort : "; pkp ;'fNL;
             'sTR "because"; 'sPC; 'sTR explanation >])
-  | None -> [<>]
+  | None -> 
+      [<>]
 
 let explain_elim_arity k ctx ind aritylst c p pt okinds = 
   let pi = P.pr_term k ctx ind in
@@ -64,63 +99,57 @@ let explain_elim_arity k ctx ind aritylst c p pt okinds =
   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
-  errorlabstrm "incorrect elimimnation arity"
-    [< '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 >]
+  [< '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
-  errorlabstrm "Cases on non inductive type"
-    [< 'sTR "In Cases expression"; 'bRK(1,1); pc; 'sPC; 
-       'sTR "has type"; 'bRK(1,1); pct; 'sPC; 
-       'sTR "which is not an inductive definition" >]
-
+  [< '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
-  errorlabstrm "Cases with wrong number of cases"
-    [< 'sTR "Cases on term"; 'bRK(1,1); pc; 'sPC ;
-       'sTR "of type"; 'bRK(1,1); pct; 'sPC;
-       'sTR "expects ";  'iNT expn; 'sTR " branches" >]
+  [< '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
-  errorlabstrm "Ill-formed branches" 
-    [< '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 >]
+  [< '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 = P.pr_ne_ctx [< 'sTR"in environment" >] k ctx in
+  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
-  errorlabstrm "P.rel"
-    [< '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." >]
+  [< '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 = P.pr_ne_ctx [< 'sTR"In environment" >] k ctx in
+  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
-  errorlabstrm "Bad cast"
-    [< 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 >]
+  [< 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 = P.pr_ne_ctx [< 'sTR"in environment" >] k ctx in
+  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
@@ -131,31 +160,28 @@ let explain_cant_apply k ctx s rator randl =
          let pct = P.pr_term k ctx c.uj_type in
          hOV 2 [< pc; 'sPC; 'sTR": " ; pct >]) randl 
   in
-  errorlabstrm "Illegal application"
-    [< '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 >]
+  [< '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
-  errorlabstrm "Ill-formed rec body"
-    [< str; 'fNL; 'sTR"The ";
-       if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">];
-       'sTR"recursive definition"; 'sPC ; pvd; 'sPC;
-       'sTR "is not well-formed" >]
+  [< str; 'fNL; 'sTR"The ";
+     if Array.length vdefs = 1 then [<>] else [<'iNT (i+1); 'sTR "-th ">];
+     'sTR"recursive definition"; '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
-  errorlabstrm "Ill-typed rec body"
-    [< '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 >]
+  [< '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_type_error k ctx = function
   | UnboundRel n -> 
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 081e23ebd..5c5548c2a 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -11,15 +11,24 @@ open Type_errors
 (*i*)
 
 (* This module provides functions to explain the various typing errors.
-   It is parameterized by functions to pretty-print terms and contexts. *)
+   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
-  val pr_ne_ctx : std_ppcmds -> path_kind -> context -> 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 \citesec{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
@@ -28,7 +37,7 @@ 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 -> 'a
+val explain_reference_variables : identifier -> std_ppcmds
 
 val explain_elim_arity : 
   path_kind -> context -> constr -> constr list -> constr 
@@ -47,8 +56,7 @@ val explain_generalization :
   path_kind -> context -> name * typed_type -> constr -> std_ppcmds
 
 val explain_actual_type :
-  path_kind -> context -> constr -> constr -> constr ->
-    std_ppcmds
+  path_kind -> context -> constr -> constr -> constr -> std_ppcmds
 
 val explain_cant_apply : 
   path_kind -> context -> string -> unsafe_judgment 
@@ -62,6 +70,4 @@ val explain_ill_typed_rec_body  :
   path_kind -> context -> int -> name list -> unsafe_judgment array 
     -> typed_type array -> std_ppcmds
 
-val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
-
 end
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index a58ce94a6..5e1c3ca58 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -9,6 +9,7 @@ open Term
 open Sign
 open Constant
 open Inductive
+open Type_errors
 open Typing
 open G_minicoq
 
@@ -44,7 +45,8 @@ let check c =
   let c = globalize [] c in
   let (j,u) = safe_machine !env c in
   let ty = j_type j in
-  mSGNL (hOV 0 [< 'sTR"  :"; 'sPC; hOV 0 (pr_term ty); 'fNL >])
+  let pty = pr_term CCI (context !env) ty in
+  mSGNL (hOV 0 [< 'sTR"  :"; 'sPC; hOV 0 pty; 'fNL >])
 
 let definition id ty c =
   let c = globalize [] c in
@@ -107,19 +109,26 @@ let parse_file f =
   with 
     | 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)
+
+let rec explain_exn = function
+  | TypeError (k,ctx,te) -> 
+      mSGNL (hOV 0 [< 'sTR "type error:"; 'sPC; 
+		      Explain.explain_type_error k ctx te; 'fNL >])
+  | Stdpp.Exc_located (_,exn) -> 
+      explain_exn exn
+  | exn -> 
+      mSGNL (hOV 0 [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >])
+
 let top () =
   let cs = Stream.of_channel stdin in
   while true do
     try
       let c = Grammar.Entry.parse command cs in execute c
     with 
-      | End_of_file | Stdpp.Exc_located (_, End_of_file) -> 
-	  exit 0
-      | Stdpp.Exc_located (_,exn) ->
-	  mSGNL [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >]
-      | exn -> 
-	  mSGNL [< 'sTR"error: "; 'sTR (Printexc.to_string exn); 'fNL >]
+      | End_of_file | Stdpp.Exc_located (_, End_of_file) -> exit 0
+      | exn -> explain_exn exn
   done
 
 let main () =