diff options
Diffstat (limited to 'toplevel/coqtop.mli')
| -rw-r--r-- | toplevel/coqtop.mli | 18 |
1 files changed, 14 insertions, 4 deletions
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli index c95d0aca55..300a7a039b 100644 --- a/toplevel/coqtop.mli +++ b/toplevel/coqtop.mli @@ -12,14 +12,24 @@ [init] is used to do custom command line argument parsing. [run] launches a custom toplevel. *) -open Coqargs + +type init_fn = opts:Coqargs.t -> string list -> Coqargs.t * string list type custom_toplevel = - { init : opts:coq_cmdopts -> string list -> coq_cmdopts * string list - ; run : opts:coq_cmdopts -> state:Vernac.State.t -> unit - ; opts : Coqargs.coq_cmdopts + { init : init_fn + ; run : opts:Coqargs.t -> state:Vernac.State.t -> unit + ; opts : Coqargs.t } +(** [init_toplevel ~help ~init custom_init arg_list] + Common Coq initialization and argument parsing *) +val init_toplevel + : help:(unit -> unit) + -> init:Coqargs.t + -> init_fn + -> string list + -> Coqargs.t * string list + val coqtop_toplevel : custom_toplevel (** The Coq main module. [start custom] will parse the command line, |