summaryrefslogtreecommitdiff
path: root/ide/coq.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coq.mli')
-rw-r--r--ide/coq.mli10
1 files changed, 6 insertions, 4 deletions
diff --git a/ide/coq.mli b/ide/coq.mli
index 40a6dea8..3af0aa69 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -134,13 +134,15 @@ val stop_worker: Interface.stop_worker_sty-> Interface.stop_worker_rty query
module PrintOpt :
sig
- type t (** Representation of an option *)
+ type 'a t (** Representation of an option *)
- type bool_descr = { opts : t list; init : bool; label : string }
+ type 'a descr = { opts : 'a t list; init : 'a; label : string }
- val bool_items : bool_descr list
+ val bool_items : bool descr list
- val set : t -> bool -> unit
+ val diff_item : string descr
+
+ val set : 'a t -> 'a -> unit
val printing_unfocused: unit -> bool