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
---
 proofs/proof_type.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'proofs')

diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 7ff1afc224..0635995352 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
-- 
cgit v1.2.3