summaryrefslogtreecommitdiff
path: root/ide/coq.mli
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
commit86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree9b221c283c2971f7ac151397231059e1d239e723 /ide/coq.mli
parent39efc41237ec906226a3a53d7396d51173495204 (diff)
parent61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)
Diffstat (limited to 'ide/coq.mli')
-rw-r--r--ide/coq.mli14
1 files changed, 9 insertions, 5 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index 9d64da6c..7f61521e 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -13,11 +13,15 @@
val short_version : unit -> string
val version : unit -> string
-(** * Initial checks by launching test coqtop processes *)
-
-val filter_coq_opts : string list -> bool * string list
-
-(** A mock coqtop launch, checking in particular that initial.coq is found *)
+(** * Launch a test coqtop processes, ask for a correct coqtop if it fails.
+ @return the list of arguments that coqtop did not understand
+ (the files probably ..). This command may terminate coqide in
+ case of trouble. *)
+val filter_coq_opts : string list -> string list
+
+(** Launch a coqtop with the user args in order to be sure that it works,
+ checking in particular that initial.coq is found. This command
+ may terminate coqide in case of trouble *)
val check_connection : string list -> unit
(** * The structure describing a coqtop sub-process *)