From a426d4db0e8e24d1559def8aac31f85b3378768e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 11 Jul 2002 15:18:48 +0000
Subject: Protection contre l'encapsulage de FailError dans Exc_located (sinon,
 par exemple, 'Try Tauto' ne marche pas)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2855 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/refiner.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index b990e6f4b2..071f14330d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -463,11 +463,10 @@ let tclORELSE0 t1 t2 g =
     t1 g
   with
   | e when catchable_exception e -> t2 g
-  | FailError lvl ->
-    if lvl = 0 then
-      t2 g
-    else
-      raise (FailError (lvl - 1))
+  | FailError 0 | Stdpp.Exc_located(_, FailError 0) -> t2 g
+  | FailError lvl -> raise (FailError (lvl - 1))
+  | Stdpp.Exc_located (s,FailError lvl) ->
+      raise (Stdpp.Exc_located (s,FailError (lvl - 1)))
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, 
    then applies t2 *)
-- 
cgit v1.2.3