aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/coq_micromega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/coq_micromega.ml')
-rw-r--r--plugins/micromega/coq_micromega.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index eff1d4ba9..082814655 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1764,7 +1764,7 @@ let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivste
Lazy.force require_csdp;
let cmdname =
- List.fold_left Filename.concat (Envars.coqlib ~fail:Errors.error)
+ List.fold_left Filename.concat (Envars.coqlib ())
["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
match ((command cmdname [|cmdname|] (provername,poly)) : csdp_certificate) with