From 033fed4d6788be791bb1c980f3cddc10827d6318 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 13 Mar 2013 00:00:59 +0000
Subject: Restrict (try...with...) to avoid catching critical exn (part 15)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16292 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/nsatz/nsatz.ml4 | 2 +-
 plugins/nsatz/utile.ml  | 7 ++++---
 2 files changed, 5 insertions(+), 4 deletions(-)

(limited to 'plugins/nsatz')

diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 7b42fc5ba8..e31eba4e06 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -54,7 +54,7 @@ module BigInt = struct
   let to_int x = int_of_big_int x
   let hash x =
     try (int_of_big_int x)
-    with _-> 1
+    with Failure _ -> 1
   let puis = power_big_int_positive_int
 
   (* a et b positifs, résultat positif *)
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index d647b14ed0..638242462c 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -51,7 +51,7 @@ let facteurs_liste div constant lp =
                                    if not (constant r)
 				   then l1:=r::(!l1)
                                    else p_dans_lmin:=true)
-			      with _ -> ())
+			      with e when Errors.noncritical e -> ())
                      lmin;
           if !p_dans_lmin
           then factor lmin lp1
@@ -62,7 +62,8 @@ let facteurs_liste div constant lp =
                 List.iter (fun q -> try (let r = div q p in
 					 if not (constant r)
 					 then l1:=r::(!l1))
-				    with _ -> lmin1:=q::(!lmin1))
+				    with e when Errors.noncritical e ->
+                                      lmin1:=q::(!lmin1))
                           lmin;
 	        factor (List.rev (p::(!lmin1))) !l1)
           (* au moins un q de lmin divise p non trivialement *)
@@ -92,7 +93,7 @@ let factorise_tableau div zero c f l1 =
       	                       li:=j::(!li);
                                r:=rr;
 			   done)
-                      with _ -> ())
+                      with e when Errors.noncritical e -> ())
                   l1;
       res.(i)<-(!r,!li))
      f;
-- 
cgit v1.2.3