Imported Upstream version 8.4pl2dfsgupstream/8.4pl2dfsg

1 files changed, 6 insertions, 4 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 74e40e3b..d299a520 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -320,10 +320,12 @@ let rec tclDISPATCHGEN null join tacs env = { go = fun sk fk step ->
 (* takes a tactic which can raise exception and makes it pure by *failing* 
     on with these exceptions. Does not catch anomalies. *)
 let purify t = 
-  let t' env = { go = fun sk fk step -> try (t env).go (fun x -> sk (Util.Inl x)) fk step
-     	                                                     with Util.Anomaly _ as e -> raise e
-							           | e -> sk (Util.Inr e) fk step
-	       }
+  let t' env =
+    { go = fun sk fk step ->
+      try (t env).go (fun x -> sk (Util.Inl x)) fk step
+      with Util.Anomaly _ as e -> raise e
+	| e when Errors.noncritical e -> sk (Util.Inr e) fk step
+    }
   in
   tclBIND t' begin function
     | Util.Inl x -> tclUNIT x