aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/coqlib.mli')
-rw-r--r--interp/coqlib.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 6741e1a0a..64c83d7eb 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -31,6 +31,9 @@ val arith_modules : string list list
val zarith_base_modules : string list list
val init_modules : string list list
+(* For tactics/commands requiring vernacular libraries *)
+val check_required_library : string list -> unit
+
(*s Global references *)
(* Modules *)