Cerrors: get rid of some FIXME

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

1 files changed, 5 insertions, 10 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index ad7b70a6e..faf698d47 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -41,10 +41,6 @@ let explain_exn_default = function
   | Timeout -> hov 0 (str "Timeout!")
   | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
   (* Meta-exceptions *)
-(*  | Loc.Exc_located (loc,exc) ->
-      hov 0 ((if Loc.is_ghost loc then (mt ())
-               else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
-               ++ Errors.print_no_anomaly exc)*)
   | EvaluatedError (msg,None) -> msg
   | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise
   (* Otherwise, not handled here *)
@@ -59,9 +55,6 @@ let wrap_vernac_error exn strm =
   let e = EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None) in
   Exninfo.copy exn e
 
-let is_mt t =
-  Pervasives.(=) (Lazy.force t) (mt ()) (* FIXME *)
-
 let rec process_vernac_interp_error exn = match exn with
   | Univ.UniverseInconsistency (o,u,v,p) ->
     let pr_rel r =
@@ -112,13 +105,15 @@ let rec process_vernac_interp_error exn = match exn with
         (str "No constant of this name:" ++ spc () ++
          Libnames.pr_qualid q ++ str ".")
   | Refiner.FailError (i,s) ->
+      let s = Lazy.force s in
       wrap_vernac_error exn
 	(str "Tactic failure" ++
-           (if not (is_mt s) then str ":" ++ Lazy.force s else mt ()) ++ (* FIXME *)
-           if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
+         (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 ".")
-  | Proof_type.LtacLocated (_,_,(Refiner.FailError (i,s) as exc)) when not (is_mt s) ->
+  | Proof_type.LtacLocated (_,_,(Refiner.FailError (i,s) as exc))
+      when not (Pp.is_empty (Lazy.force s)) ->
       (* Ltac error is intended, trace is irrelevant *)
       process_vernac_interp_error exc
   | Proof_type.LtacLocated (s,loc,exc) ->