From 08e7ec2c48c5ca666ad42b5f969576e6aa43d2ea Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 22 Aug 2013 14:29:58 +0000
Subject: Misc changes around coqtop.ml :

 - Revised Coqtop.parse_args in a cleaner and lighter style
 - Improved error message in case of argument parse failure:
   * tell which option is expecting a related argument
   * in case of unknown options, warn about them all at once
   * do not hide the previous error messages by filling the
     screen with usage(). Instead, suggest the use of --help.
 - Specialized boolean config field Coq_config.arch_is_win32
 - Faster Envars.coqlib, which is back to (unit->string), and
   just access Flags.coqlib. Caveat: it must be initialized once
   via Envars.set_coqlib
 - Avoid keeping an opened channel to the "revision" file
 - Direct load of theories/init/prelude.vo, no detour via Loadpath

Beware : ./configure must be runned after this commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16726 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/micromega/coq_micromega.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index eff1d4ba99..082814655c 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
-- 
cgit v1.2.3