From 923ce36ed6789718746369847f622b17bb37df2a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 18 May 2015 15:29:55 +0200
Subject: Tentative fix for #3461: Anomaly: Uncaught exception
 Pretype_errors.PretypeError.

Instad of trying to print the exception, we raise it in the tactic monad.
---
 proofs/clenvtac.ml            | 4 +---
 test-suite/bugs/closed/3461.v | 5 +++++
 test-suite/bugs/opened/3461.v | 5 -----
 3 files changed, 6 insertions(+), 8 deletions(-)
 create mode 100644 test-suite/bugs/closed/3461.v
 delete mode 100644 test-suite/bugs/opened/3461.v

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 18883df247..aaa49f1169 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -125,7 +125,5 @@ let unify ?(flags=fail_quick_unif_flags) m =
     try
       let evd' = w_unify env evd CONV ~flags m n in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
-    with e when Errors.noncritical e ->
-      (** This is Tacticals.tclFAIL *)
-      Proofview.tclZERO (FailError (0, lazy (Errors.print e)))
+    with e when Errors.noncritical e -> Proofview.tclZERO e
   end
diff --git a/test-suite/bugs/closed/3461.v b/test-suite/bugs/closed/3461.v
new file mode 100644
index 0000000000..1b625e6a15
--- /dev/null
+++ b/test-suite/bugs/closed/3461.v
@@ -0,0 +1,5 @@
+Lemma foo (b : bool) :
+  exists x : nat, x = x.
+Proof.
+eexists. 
+Fail eexact (eq_refl b).
diff --git a/test-suite/bugs/opened/3461.v b/test-suite/bugs/opened/3461.v
deleted file mode 100644
index 1b625e6a15..0000000000
--- a/test-suite/bugs/opened/3461.v
+++ /dev/null
@@ -1,5 +0,0 @@
-Lemma foo (b : bool) :
-  exists x : nat, x = x.
-Proof.
-eexists. 
-Fail eexact (eq_refl b).
-- 
cgit v1.2.3