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

7 files changed, 19 insertions, 21 deletions

diff --git a/lib/errors.ml b/lib/errors.ml
index 157949fcd..ae188cfeb 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -110,10 +110,6 @@ let print_no_report e = print_gen (print_anomaly false) !handle_stack e
 
 let print_anomaly e = print_anomaly true e
 
-(** Same as [print], except that anomalies are not printed but re-raised
-    (used for the Fail command) *)
-let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e
-
 (** Predefined handlers **)
 
 let _ = register_handler begin function
diff --git a/lib/errors.mli b/lib/errors.mli
index c5400574b..a7f4ef0cd 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -81,10 +81,6 @@ val print_anomaly : exn -> Pp.std_ppcmds
     isn't printed (used in Ltac debugging). *)
 val print_no_report : exn -> Pp.std_ppcmds
 
-(** Same as [print], except that anomalies are not printed but re-raised
-    (used for the Fail command) *)
-val print_no_anomaly : exn -> Pp.std_ppcmds
-
 (** Critical exceptions shouldn't be catched and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
     only at the very end of interp, to be displayed to the user.
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 7ff1afc22..063599535 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -82,4 +82,7 @@ type ltac_call_kind =
 
 type ltac_trace = (int * Loc.t * ltac_call_kind) list
 
+(** Invariant: the exceptions embedded in LtacLocated satisfy
+    Errors.noncritical *)
+
 exception LtacLocated of ltac_trace * Loc.t * exn
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e52d78411..08de6cb02 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -81,8 +81,10 @@ let catch_error call_trace tac g =
     [], loc, e
   in
   if List.is_empty call_trace & List.is_empty inner_trace then raise e
-  else
+  else begin
+    assert (Errors.noncritical e); (* preserved invariant about LtacLocated *)
     raise (LtacLocated(inner_trace@call_trace,loc,e))
+  end
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign =
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