aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coq.mli
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-28 09:49:48 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-28 09:49:48 +0000
commit7828a2e3c8361b0f04a2bd4fd0127ffcdc87153b (patch)
treed02f238a673ee62853e359c8e5f69247c84f3e8e /ide/coq.mli
parentc2c3b8cb7c2364c6effc89ab73b3e50874fc616c (diff)
Ide: new option -coqtop <mycoqtop> + remove wrong quoting of args
* Run "coqide -coqtop someothercoqtop" if you want to use a toplevel which isn't the one coming alongside coqide. To be documented, to be improved (maybe an field in coqide's preferences ?). coqide -h should display this kind of ide-specific option. * Since we now use create_process instead of open_process, we don't use /bin/sh, hence running Filename.quote on args was actually wrong. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13932 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
-rw-r--r--ide/coq.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index 37c5bcd00..f04dfeede 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -9,8 +9,10 @@
val short_version : unit -> string
val version : unit -> string
val filter_coq_opts : string list -> bool * string list
+(* A mock coqtop launch, checking in particular that initial.coq is found *)
val check_connection : string list -> unit
-val coqlib : unit -> string
+(* Same, with less checks, but returning coqlib *)
+val check_coqlib : string list -> string
type coqtop