aboutsummaryrefslogtreecommitdiff
path: root/toplevel/ccompile.mli
diff options
context:
space:
mode:
authorEnrico Tassi2021-01-05 11:34:35 +0100
committerEnrico Tassi2021-01-27 09:45:49 +0100
commit4264aec518d5407f345c58e18e014e15e9ae96af (patch)
tree03209892ae2549f171af39efa5d6925b745d54ec /toplevel/ccompile.mli
parent4390b6907b3d07793c2e8f9e7ad3cc38d9488711 (diff)
[sysinit] new component for system initialization
This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml
Diffstat (limited to 'toplevel/ccompile.mli')
-rw-r--r--toplevel/ccompile.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/ccompile.mli b/toplevel/ccompile.mli
index 8c154488d0..1b670a8edc 100644
--- a/toplevel/ccompile.mli
+++ b/toplevel/ccompile.mli
@@ -13,7 +13,7 @@
val load_init_vernaculars : Coqargs.t -> state:Vernac.State.t-> Vernac.State.t
(** [compile_files opts] compile files specified in [opts] *)
-val compile_files : Coqargs.t -> Coqcargs.t -> unit
+val compile_files : Coqargs.t * Stm.AsyncOpts.stm_opt -> Coqcargs.t -> unit
(** [do_vio opts] process [.vio] files in [opts] *)
val do_vio : Coqargs.t -> Coqcargs.t -> unit