diff options
| author |  fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-20 09:13:31 +0000 |
|---|---|---|
| committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-20 09:13:31 +0000 |
| commit | f3ac2308f8ed6f9a02df6e78a804cdbf54a62cea (patch) | |
| tree | c0e731d39eb49bae78898664fa527bc07db625e0 /plugins/micromega/coq_micromega.ml | |
| parent | 05ba7289d4fc9b3b816ecbfabc76656107ee1015 (diff) | |
new csdp cache + improved error message
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12286 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
| -rw-r--r-- | plugins/micromega/coq_micromega.ml | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 286e866fd..acef98e78 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1322,8 +1322,8 @@ let lift_ratproof prover l = | None -> None | Some c -> Some (Mc.RatProof( c,Mc.DoneProof)) -type csdpcert = Sos.positivstellensatz option -type micromega_polys = (Mc.q Mc.pol * Mc.op1) list +type micromega_polys = (Micromega.q Mc.pol * Mc.op1) list +type csdp_certificate = S of Sos.positivstellensatz option | F of string type provername = string * int option open Persistent_cache @@ -1336,14 +1336,19 @@ end) let csdp_cache = "csdp.cache" -let really_call_csdpcert : provername -> micromega_polys -> csdpcert = +let really_call_csdpcert : provername -> micromega_polys -> Sos.positivstellensatz option = fun provername poly -> let cmdname = List.fold_left Filename.concat (Envars.coqlib ()) ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in - command cmdname [| cmdname |] (provername,poly) + match command cmdname [| cmdname |] (provername,poly) with + | None -> failwith "unix error" + | Some res -> + match res with + | F str -> failwith str + | S res -> res |