From 2f8bc98ab583a7259e167cd6bf3bce36aa33ada6 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 14 Mar 2013 17:43:06 +0000
Subject: 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
---
 tactics/tacinterp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e52d784114..08de6cb027 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 =
-- 
cgit v1.2.3