Do not prepend a "Error:" header when the error is expected by the user.

This commit also removes the extraneous "=>" token from Fail messages and
prevents them from losing all the formatting information.

1 files changed, 24 insertions, 21 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 2df7c2273..b29ba1efc 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -52,12 +52,15 @@ let _ = Errors.register_handler explain_exn_default
 
 (** Pre-explain a vernac interpretation error *)
 
-let wrap_vernac_error (exn, info) strm =
-  let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
-  let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
-  (e, info)
+let wrap_vernac_error with_header (exn, info) strm =
+  if with_header then
+    let header = Pp.tag (Pp.Tag.inj Ppstyle.error_tag Ppstyle.tag) (str "Error:") in
+    let e = EvaluatedError (hov 0 (header ++ spc () ++ strm), None) in
+    (e, info)
+  else
+    (EvaluatedError (strm, None), info)
 
-let process_vernac_interp_error exn = match fst exn with
+let process_vernac_interp_error with_header exn = match fst exn with
   | Univ.UniverseInconsistency i ->
     let msg =
       if !Constrextern.print_universes then
@@ -65,40 +68,40 @@ let process_vernac_interp_error exn = match fst exn with
 	  Univ.explain_universe_inconsistency Universes.pr_with_global_universes i
       else
 	mt() in
-    wrap_vernac_error exn (str "Universe inconsistency" ++ msg ++ str ".")
+    wrap_vernac_error with_header exn (str "Universe inconsistency" ++ msg ++ str ".")
   | TypeError(ctx,te) ->
-      wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
+      wrap_vernac_error with_header exn (Himsg.explain_type_error ctx Evd.empty te)
   | PretypeError(ctx,sigma,te) ->
-      wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
+      wrap_vernac_error with_header exn (Himsg.explain_pretype_error ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, te) ->
-      wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
+      wrap_vernac_error with_header exn (Himsg.explain_typeclass_error env te)
   | InductiveError e ->
-      wrap_vernac_error exn (Himsg.explain_inductive_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_inductive_error e)
   | Modops.ModuleTypingError e ->
-      wrap_vernac_error exn (Himsg.explain_module_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_module_error e)
   | Modintern.ModuleInternalizationError e ->
-      wrap_vernac_error exn (Himsg.explain_module_internalization_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_module_internalization_error e)
   | RecursionSchemeError e ->
-      wrap_vernac_error exn (Himsg.explain_recursion_scheme_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_recursion_scheme_error e)
   | Cases.PatternMatchingError (env,sigma,e) ->
-      wrap_vernac_error exn (Himsg.explain_pattern_matching_error env sigma e)
+      wrap_vernac_error with_header exn (Himsg.explain_pattern_matching_error env sigma e)
   | Tacred.ReductionTacticError e ->
-      wrap_vernac_error exn (Himsg.explain_reduction_tactic_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_reduction_tactic_error e)
   | Logic.RefinerError e ->
-      wrap_vernac_error exn (Himsg.explain_refiner_error e)
+      wrap_vernac_error with_header exn (Himsg.explain_refiner_error e)
   | Nametab.GlobalizationError q ->
-      wrap_vernac_error exn
+      wrap_vernac_error with_header exn
         (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
 	 spc () ++ str "was not found" ++
 	 spc () ++ str "in the current" ++ spc () ++ str "environment.")
   | Refiner.FailError (i,s) ->
       let s = Lazy.force s in
-      wrap_vernac_error exn
+      wrap_vernac_error with_header exn
 	(str "Tactic failure" ++
          (if Pp.is_empty s then s else str ": " ++ s) ++
          if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
   | AlreadyDeclared msg ->
-      wrap_vernac_error exn (msg ++ str ".")
+      wrap_vernac_error with_header exn (msg ++ str ".")
   | _ ->
       exn
 
@@ -107,9 +110,9 @@ let rec strip_wrapping_exceptions = function
     strip_wrapping_exceptions e
   | exc -> exc
 
-let process_vernac_interp_error (exc, info) =
+let process_vernac_interp_error ?(with_header=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
-  let e = process_vernac_interp_error (exc, info) in
+  let e = process_vernac_interp_error with_header (exc, info) in
   let ltac_trace = Exninfo.get info Proof_type.ltac_trace_info in
   let loc = Option.default Loc.ghost (Loc.get_loc info) in
   match ltac_trace with