diff options
| author | letouzey | 2013-03-13 00:00:59 +0000 |
|---|---|---|
| committer | letouzey | 2013-03-13 00:00:59 +0000 |
| commit | 033fed4d6788be791bb1c980f3cddc10827d6318 (patch) | |
| tree | 42184b7d27f439e74aee474c34afd623b9d91087 /plugins/nsatz | |
| parent | 8d70a84682ded179c461e633c7865486c63e55db (diff) | |
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
Diffstat (limited to 'plugins/nsatz')
| -rw-r--r-- | plugins/nsatz/nsatz.ml4 | 2 | ||||
| -rw-r--r-- | plugins/nsatz/utile.ml | 7 |
2 files changed, 5 insertions, 4 deletions
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; |