From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 27 Mar 2006 12:21:48 +0000 (+0000)
Subject: Several "try ... with _ -> " specialized.
X-Git-Tag: make_still_working~7458
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fecaa410b6226e8614cfef78d0f952e3c676c06e;hp=35e2f71ae7a80947ea53282418034674c3538c32;p=helm.git

Several "try ... with _ -> " specialized.
---

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index 954134584..2a7a3f2d0 100644
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -119,7 +119,8 @@ let rec pp t l =
               name ^ pp_exp_named_subst exp_named_subst l
           | _ -> raise CicPpInternalError
         with
-         _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
+           Sys.Break as exn -> raise exn
+         | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
        )
     | C.MutConstruct (uri,n1,n2,exp_named_subst) ->
        (try
@@ -130,7 +131,8 @@ let rec pp t l =
                id ^ pp_exp_named_subst exp_named_subst l
           | _ -> raise CicPpInternalError
         with
-         _ ->
+           Sys.Break as exn -> raise exn
+         | _ ->
           UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
            string_of_int n2
        )
diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 046ab908a..18259a004 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -357,7 +357,7 @@ module Reduction(RS : Strategy) =
            let d =
             try
              Some (RS.from_env_for_unwind ~unwind (List.nth e (n-m-1)))
-            with _ -> None
+            with Failure _ -> None
            in
             (match d with 
                 Some t' ->
@@ -682,7 +682,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
           try
            Some (RS.from_stack (List.nth s recindex))
           with
-           _ -> None
+           Failure _ -> None
          in
           (match recparam with
               Some recparam ->
diff --git a/helm/software/components/cic_proof_checking/cicTypeChecker.ml b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
index 951f68dbd..c4b7f8cbf 100644
--- a/helm/software/components/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/software/components/cic_proof_checking/cicTypeChecker.ml
@@ -1472,7 +1472,7 @@ and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
           | None -> raise 
 	      (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
         with
-        _ ->
+        Failure _ ->
           raise (TypeCheckerFailure (lazy "unbound variable"))
        )
     | C.Var (uri,exp_named_subst) ->