aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/csdpcert.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-13 00:00:59 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-13 00:00:59 +0000
commit033fed4d6788be791bb1c980f3cddc10827d6318 (patch)
tree42184b7d27f439e74aee474c34afd623b9d91087 /plugins/micromega/csdpcert.ml
parent8d70a84682ded179c461e633c7865486c63e55db (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/micromega/csdpcert.ml')
-rw-r--r--plugins/micromega/csdpcert.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index f848591cc..6fd79f16b 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.ml
@@ -148,7 +148,7 @@ let real_nonlinear_prover d l =
S (Some proof)
with
| Sos_lib.TooDeep -> S None
- | x -> F (Printexc.to_string x)
+ | any -> F (Printexc.to_string any)
(* This is somewhat buggy, over Z, strict inequality vanish... *)
let pure_sos l =
@@ -172,7 +172,7 @@ let pure_sos l =
S (Some proof)
with
(* | Sos.CsdpNotFound -> F "Sos.CsdpNotFound" *)
- | x -> (* May be that could be refined *) S None
+ | any -> (* May be that could be refined *) S None
@@ -201,7 +201,7 @@ let main () =
Marshal.to_channel chan (cert:csdp_certificate) [] ;
flush chan ;
exit 0
- with x -> (Printf.fprintf chan "error %s" (Printexc.to_string x) ; exit 1)
+ with any -> (Printf.fprintf chan "error %s" (Printexc.to_string any) ; exit 1)
;;