diff options
Diffstat (limited to 'ide/ideutils.mli')
| -rw-r--r-- | ide/ideutils.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 5877d1270..657e92869 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -40,9 +40,6 @@ val stock_to_widget : ?size:[`CUSTOM of int * int | Gtk.Tags.icon_size] -> GtkStock.id -> GObj.widget -open Format -val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit - val custom_coqtop : string option ref (* @return command to call coqtop - custom_coqtop if set |