Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncritical

 This was apparently already the case before, but this invariant is now
 explicited in comments + a few asserts.

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

3 files changed, 13 insertions, 12 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index faf698d47..de4a614c9 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -23,6 +23,8 @@ let print_loc loc =
 
 let guill s = "\""^s^"\""
 
+(** Invariant : exceptions embedded in EvaluatedError satisfy
+    Errors.noncritical *)
 
 exception EvaluatedError of std_ppcmds * exn option
 
@@ -40,9 +42,9 @@ let explain_exn_default = function
   | Stack_overflow -> hov 0 (str "Stack overflow.")
   | Timeout -> hov 0 (str "Timeout!")
   | Sys.Break -> hov 0 (fnl () ++ str "User interrupt.")
-  (* Meta-exceptions *)
+  (* Exceptions with pre-evaluated error messages *)
   | EvaluatedError (msg,None) -> msg
-  | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print_no_anomaly reraise
+  | EvaluatedError (msg,Some reraise) -> msg ++ Errors.print reraise
   (* Otherwise, not handled here *)
   | _ -> raise Errors.Unhandled
 
@@ -117,12 +119,11 @@ let rec process_vernac_interp_error exn = match exn with
       (* Ltac error is intended, trace is irrelevant *)
       process_vernac_interp_error exc
   | Proof_type.LtacLocated (s,loc,exc) ->
-      (match
-          Himsg.extract_ltac_trace s loc (process_vernac_interp_error exc)
-       with
-       | None,loc,e -> Loc.add_loc e loc
-       | Some msg, loc, e ->
-        Loc.add_loc (EvaluatedError (msg,Some e)) loc)
+      let e = process_vernac_interp_error exc in
+      assert (Errors.noncritical e);
+      (match Himsg.extract_ltac_trace s loc with
+        | None,loc -> Loc.add_loc e loc
+        | Some msg, loc -> Loc.add_loc (EvaluatedError (msg,Some e)) loc)
   | exc ->
       exc
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 87df8a055..2759c677b 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1093,13 +1093,13 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
   else
     mt ()
 
-let extract_ltac_trace trace eloc e =
+let extract_ltac_trace trace eloc =
   let (nrep,loc,c),tail = List.sep_last trace in
   if is_defined_ltac trace then
     (* We entered a user-defined tactic,
        we display the trace with location of the call *)
     let msg = hov 0 (explain_ltac_call_trace (nrep,c,tail,eloc) ++ fnl()) in
-    Some msg, loc, e
+    Some msg, loc
   else
     (* We entered a primitive tactic, we don't display trace but
        report on the finest location *)
@@ -1111,4 +1111,4 @@ let extract_ltac_trace trace eloc e =
         | _::tail -> aux tail
         | [] -> Loc.ghost in
         aux trace in
-    None, best_loc, e
+    None, best_loc
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index bd7fb8973..9ec344405 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -38,7 +38,7 @@ val explain_reduction_tactic_error :
   Tacred.reduction_tactic_error -> std_ppcmds
 
 val extract_ltac_trace :
-  Proof_type.ltac_trace -> Loc.t -> exn -> std_ppcmds option * Loc.t * exn
+  Proof_type.ltac_trace -> Loc.t -> std_ppcmds option * Loc.t
 
 val explain_module_error : Modops.module_typing_error -> std_ppcmds