aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/nsatz/ideal.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-13 00:00:12 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-13 00:00:12 +0000
commit552df1605233769ad3cdabaadaa0011605e79797 (patch)
tree28c3ae6a250aba80e1eb53ff9d906df9f49b75c1 /plugins/nsatz/ideal.ml
parentda3cbbcef1f4de9780603225e095f026bb5da709 (diff)
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
Diffstat (limited to 'plugins/nsatz/ideal.ml')
-rw-r--r--plugins/nsatz/ideal.ml4
1 files changed, 2 insertions, 2 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)