From bc77fdc4330c8572111102d61fd65f032b1cf5b6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 2 Mar 2020 23:51:17 +0100
Subject: Double-checking at tclZERO entry that the exception is non critical.

---
 engine/proofview.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 6a4e490408..d20c660311 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -262,6 +262,8 @@ module Monad = Proof
 
 (** [tclZERO e] fails with exception [e]. It has no success. *)
 let tclZERO ?info e =
+  if not (CErrors.noncritical e) then
+    CErrors.anomaly (Pp.str "tclZERO receiving critical error: " ++ CErrors.print e);
   let info = match info with
   | None -> Exninfo.null
   | Some info -> info
-- 
cgit v1.2.3