rattrapage exceptions autres que UserError

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@254 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 37 insertions, 18 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 3555a386a5..0a44eff874 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -153,7 +153,7 @@ let unify_0 mc wc m n =
 		
 	| _ -> error_cannot_unify CCI (m,n)
 	      
-    with UserError _ as ex ->
+    with ex when catchable_exception ex ->
       if (not(occur_meta cM)) & w_conv_x wc cM cN then 
 	substn
       else 
@@ -250,7 +250,7 @@ and w_resrec metas evars wc =
 	else
           (try 
 	     w_resrec metas t (w_Define evn rhs wc)
-           with UserError _ ->
+           with ex when catchable_exception ex ->
              (match rhs with
              	| DOPN(AppL,cl) ->
 		    (match cl.(0) with
@@ -565,7 +565,7 @@ and clenv_resrec metas evars clenv =
     	else
           (try 
 	     clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv)
-           with UserError _ ->
+           with ex when catchable_exception ex ->
              (match rhs with
 		| DOPN(AppL,cl) ->
 		    (match cl.(0) with
@@ -675,18 +675,27 @@ let constrain_clenv_to_subterm clause = function
 	   if closed0 cl 
 	   then clenv_unify op cl clause,cl
            else error "Bound 1"
-	 with UserError _ ->
+	 with ex when catchable_exception ex ->
            (match telescope_appl cl with 
 	      | DOPN(AppL,tl) ->
 		  if Array.length tl = 2 then
                	    let c1 = tl.(0) and c2 = tl.(1) in
-		    (try matchrec c1 with UserError(_) -> matchrec c2)
+		    (try 
+		       matchrec c1 
+		     with ex when catchable_exception ex -> 
+		       matchrec c2)
 		  else 
 		    error "Match_subterm"
               | DOP2(Prod,t,DLAM(_,c)) ->
-		  (try matchrec t with UserError(_) -> matchrec c)
+		  (try 
+		     matchrec t 
+		   with ex when catchable_exception ex -> 
+		     matchrec c)
               | DOP2(Lambda,t,DLAM(_,c)) ->
-		  (try matchrec t with UserError(_) -> matchrec c)
+		  (try 
+		     matchrec t 
+		   with ex when catchable_exception ex -> 
+		     matchrec c)
               | _ -> error "Match_subterm")) 
       in 
       matchrec cl
@@ -700,7 +709,7 @@ let constrain_clenv_using_subterm_list allow_K clause oplist t =
          let (clause',cl) =
            (try 
 	      constrain_clenv_to_subterm clause (strip_outer_cast op,t)
-            with (UserError _ as e) ->
+            with e when catchable_exception e ->
               if allow_K then (clause,op) else raise e)
          in 
 	 (clause',cl::l)
@@ -919,7 +928,7 @@ and clenv_resrec metas evars clenv =
     	else
           (try 
 	     clenv_resrec metas t (clenv_wtactic (w_Define evn rhs) clenv)
-           with UserError _ ->
+           with ex when catchable_exception ex ->
              (match rhs with
 		| DOPN(AppL,cl) ->
 		    (match cl.(0) with
@@ -1023,19 +1032,19 @@ let clenv_unique_resolver allow_K clenv gls =
     | ((DOP0(Meta _) as pathd,_),(DOP2(Lambda,_,_) as glhd,_)) ->
 	(try 
 	   clenv_typed_fo_resolver clenv gls
-	 with UserError (t1,t2) -> 
+	 with ex when catchable_exception ex -> 
 	   try 
 	     clenv_so_resolver allow_K clenv gls
-	   with UserError (s1,s2) -> 
+	   with ex when catchable_exception ex -> 
 	     error "Cannot solve a second-order unification problem")
 
     | ((DOP0(Meta _),_),_) -> 
 	(try 
 	   clenv_so_resolver allow_K clenv gls
-         with UserError (t1,t2) -> 
+         with ex when catchable_exception ex -> 
            try 
 	     clenv_typed_fo_resolver clenv gls
-           with UserError (s1,s2) -> 
+           with ex when catchable_exception ex -> 
              error "Cannot solve a second-order unification problem")
 
     | _ -> clenv_fo_resolver clenv gls
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index e43d519665..ec23d32585 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -115,7 +115,8 @@ let w_Underlying wc = (ts_it (ids_it wc)).decls
 let w_type_of wc c  = ctxt_type_of (ids_it wc) c
 let w_env     wc    = get_env (ids_it wc)
 let w_hyps    wc    = var_context (get_env (ids_it wc))
-let w_ORELSE wt1 wt2 wc = try wt1 wc with UserError _ -> wt2 wc
+let w_ORELSE wt1 wt2 wc = 
+  try wt1 wc with e when catchable_exception e -> wt2 wc
 
 let w_Declare sp c (wc:walking_constraints) =
   begin match c with 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 8a04322828..027ceab4a4 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -13,6 +13,7 @@ open Reduction
 open Typing
 open Proof_trees
 open Typeops
+open Type_errors
 open Coqast
 open Declare
 
@@ -27,6 +28,13 @@ type refiner_error =
 
 exception RefinerError of refiner_error
 
+let catchable_exception = function
+  | Util.UserError _ | TypeError _ | RefinerError _
+  | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _)) -> 
+      true
+  | _ -> 
+      false
+
 let error_cannot_unify k (m,n) =
   raise (RefinerError (CannotUnify (m,n)))
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 4d1c2de979..7df383a738 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -36,6 +36,8 @@ exception RefinerError of refiner_error
 
 val error_cannot_unify : path_kind -> constr * constr -> 'a
 
+val catchable_exception : exn -> bool
+
 
 (*s Pretty-printer. *)
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 4b3b797bf8..137486bb48 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -60,7 +60,7 @@ let get_evmap_sign og =
         try
           let pftree = get_pftreestate () in
           Some (nth_goal_of_pftreestate 1 pftree)
-        with UserError _ -> 
+        with e when Logic.catchable_exception e -> 
 	  None 
   in
   match og with
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index c1f3331d66..c4cab5b6b9 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -460,8 +460,7 @@ let tclNOTSAMEGOAL (tac:tactic) goal =
 let tclORELSE0 t1 t2 g =
   try 
     t1 g
-  with UserError _ | TypeError _ | RefinerError _
-     | Stdpp.Exc_located(_,(UserError _ | TypeError _ | RefinerError _)) -> 
+  with e when catchable_exception e -> 
     t2 g
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, 
@@ -907,7 +906,7 @@ let tclINFO (tac:tactic) gls =
     mSGNL(hOV 0 [< 'sTR" == "; 
                    print_subscript 
                      ((compose ts_it sig_sig) gls) sign pf >])
-  with UserError _ -> 
+  with e when catchable_exception e -> 
     mSGNL(hOV 0 [< 'sTR "Info failed to apply validation" >])
   end;
   res