Restrict (try...with...) to avoid catching critical exn (part 7)

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

4 files changed, 10 insertions, 33 deletions

diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 94b79503a..5ad546588 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.ml
@@ -236,7 +236,7 @@ open Format
 
 let getvar lv i =
   try (List.nth lv i)
-  with _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv)
+  with Failure _ -> (List.fold_left (fun r x -> r^" "^x) "lv= " lv)
     ^" i="^(string_of_int i)
 
 let string_of_pol zeroP hdP tlP coefterm monterm string_of_coef
@@ -589,7 +589,7 @@ let coefpoldep = Hashtbl.create 51
 (* coef of q in p = sum_i c_i*q_i *)
 let coefpoldep_find p q =
   try (Hashtbl.find coefpoldep (p.num,q.num))
-  with _ -> []
+  with Not_found -> []
 
 let coefpoldep_remove p q =
   Hashtbl.remove coefpoldep (p.num,q.num)
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index ce70a0ffb..ca6d305e8 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.ml
@@ -163,17 +163,12 @@ let max_var l = Array.fold_right (fun p m -> max (max_var_pol2 p) m) l 0
 
 (* equality between polynomials *)
 
+exception Failed
+
 let rec equal p q =
   match (p,q) with
       (Pint a,Pint b) -> C.equal a b
-    |(Prec(x,p1),Prec(y,q1)) ->
-       if x<>y then false
-       else if (Array.length p1)<>(Array.length q1) then false
-       else (try (Array.iteri (fun i a -> if not (equal a q1.(i))
-			       then failwith "raté")
-		    p1;
-		  true)
-	     with _ -> false)
+    |(Prec(x,p1),Prec(y,q1)) -> (x=y) && Array.for_all2 equal p1 q1
     | (_,_) -> false
 
 (* normalize polynomial: remove head zeros, coefficients are normalized
@@ -519,12 +514,11 @@ let divP p q=
 
 let div_pol_rat p q=
   let x = max (max_var_pol p) (max_var_pol q) in
-    try (let s = div_pol (multP p (puisP (Pint(coef_int_tete q))
-				     (1+(deg x p) - (deg x q))))
-		   q x in
-         (* degueulasse, mais c 'est pour enlever un warning *)
-         if s==s then true else true)
-    with _ -> false
+  try
+    let r = puisP (Pint(coef_int_tete q)) (1+(deg x p)-(deg x q)) in
+    let _ = div_pol (multP p r) q x in
+    true
+  with Failure _ -> false
 
 (***********************************************************************
   5. Pseudo-division and gcd with subresultants.
diff --git a/plugins/nsatz/utile.ml b/plugins/nsatz/utile.ml
index c16bd4256..d647b14ed 100644
--- a/plugins/nsatz/utile.ml
+++ b/plugins/nsatz/utile.ml
@@ -26,19 +26,6 @@ let set_of_list_eq eq l =
    List.iter (fun x -> if not (list_mem_eq eq x (!res)) then res:=x::(!res)) l;
    List.rev !res
 
-
-(* Memoization
-   f is compatible with nf: f(nf(x)) = f(x)
-*)
-
-let memos s memoire nf f x =
-   try (let v = Hashtbl.find memoire (nf x) in pr s;v)
-   with _ -> (pr "#";
-	      let v = f x in
-	      Hashtbl.add memoire (nf x) v;
-	      v)
-
-
 (**********************************************************************
   Eléments minimaux pour un ordre partiel de division.
   E est un ensemble, avec une multiplication
diff --git a/plugins/nsatz/utile.mli b/plugins/nsatz/utile.mli
index 83b2ac39b..1f8415752 100644
--- a/plugins/nsatz/utile.mli
+++ b/plugins/nsatz/utile.mli
@@ -10,10 +10,6 @@ val info : string -> unit
 val list_mem_eq : ('a -> 'b -> bool) -> 'a -> 'b list -> bool
 val set_of_list_eq : ('a -> 'a -> bool) -> 'a list -> 'a list
 
-(* Memoization *)
-val memos :
-  string -> ('a, 'b) Hashtbl.t -> ('c -> 'a) -> ('c -> 'b) -> 'c -> 'b
-
 
 val facteurs_liste : ('a -> 'a -> 'a) -> ('a -> bool) -> 'a list -> 'a list
 val factorise_tableau :