aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.mli
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/coqinit.mli')
-rw-r--r--toplevel/coqinit.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 3b42289ee..787dfb61a 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -25,4 +25,4 @@ val init_library_roots : unit -> unit
val init_ocaml_path : unit -> unit
-val get_compat_version : string -> Flags.compat_version
+val get_compat_version : ?allow_old:bool -> string -> Flags.compat_version