From 2d8cbed59f1bafb68f188d055138d3c7d02d9e37 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Sat, 14 Apr 2001 03:16:59 +0000
Subject: Reparation du bug de Try

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1591 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.ml    | 7 +++----
 proofs/refiner.ml  | 1 +
 toplevel/errors.ml | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/proofs/logic.ml b/proofs/logic.ml
index b06f16682c..e26733a15d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -60,10 +60,9 @@ exception RefinerError of refiner_error
 
 let catchable_exception = function
   | Util.UserError _ | TypeError _ | RefinerError _
-  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _)) -> 
-      true
-  | _ -> 
-      false
+  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ |
+    Nametab.GlobalizationError _)) -> true
+  | _ -> false
 
 let error_cannot_unify k (m,n) =
   raise (RefinerError (CannotUnify (m,n)))
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 8e358adea2..eb7118398e 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -432,6 +432,7 @@ let tclORELSE0 t1 t2 g =
     t1 g
   with
   | e when catchable_exception e -> t2 g
+  | _ -> failwith "ICI!"
   | FailError lvl ->
     if lvl = 0 then
       t2 g
diff --git a/toplevel/errors.ml b/toplevel/errors.ml
index 3c18bf619e..11e7c38ccd 100644
--- a/toplevel/errors.ml
+++ b/toplevel/errors.ml
@@ -67,7 +67,7 @@ let rec explain_exn_default = function
       hOV 0 [< 'sTR "Error: Universe Inconsistency." >]
   | TypeError(k,ctx,te) -> 
       hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error k ctx te >]
-  | PretypeError(ctx,te) -> 
+  | PretypeError(ctx,te) ->
       hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_pretype_error ctx te >]
   | InductiveError e -> 
       hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_inductive_error e >]
-- 
cgit v1.2.3