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.

3 files changed, 29 insertions, 27 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
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 1768af118..100b3772c 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -12,7 +12,7 @@ val print_loc : Loc.t -> Pp.std_ppcmds
 
 (** Pre-explain a vernac interpretation error *)
 
-val process_vernac_interp_error : Util.iexn -> Util.iexn
+val process_vernac_interp_error : ?with_header:bool -> Util.iexn -> Util.iexn
 
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1b8fdd8ae..52b4dc8cf 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -2062,7 +2062,7 @@ let locate_if_not_already loc (e, info) =
   | Some l -> if Loc.is_ghost l then (e, Loc.add_loc info loc) else (e, info)
 
 exception HasNotFailed
-exception HasFailed of string
+exception HasFailed of std_ppcmds
 
 let with_fail b f =
   if not b then f ()
@@ -2077,8 +2077,8 @@ let with_fail b f =
            | HasNotFailed as e -> raise e
            | e ->
               let e = Errors.push e in
-              raise (HasFailed (Pp.string_of_ppcmds
-              (Errors.iprint (Cerrors.process_vernac_interp_error e)))))
+              raise (HasFailed (Errors.iprint
+                (Cerrors.process_vernac_interp_error ~with_header:false e))))
         ()
     with e when Errors.noncritical e -> 
       let (e, _) = Errors.push e in
@@ -2087,8 +2087,7 @@ let with_fail b f =
           errorlabstrm "Fail" (str "The command has not failed!")
       | HasFailed msg ->
           if is_verbose () || !Flags.ide_slave then msg_info
-    	(str "The command has indeed failed with message:" ++
-    	 fnl () ++ str "=> " ++ hov 0 (str msg))
+            (str "The command has indeed failed with message:" ++ fnl () ++ msg)
       | _ -> assert false
   end