diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:43:50 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-29 14:43:50 +0200 |
| commit | c3bc1fda9c5dd1805b23d04f2dee711aeec1f4a1 (patch) | |
| tree | b62cd62e04d2e965ebc2d19da69fb42ad5d0bd3b /toplevel/coqinit.mli | |
| parent | 9326b0466cc04175436dc57cf0283c151b587e54 (diff) | |
| parent | 1c55826018c5f07ee25b5771e59fe0389293cb62 (diff) | |
Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.
Diffstat (limited to 'toplevel/coqinit.mli')
| -rw-r--r-- | toplevel/coqinit.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index bf8558d10..3432e79cc 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -24,5 +24,3 @@ val init_load_path : unit -> unit val init_library_roots : unit -> unit val init_ocaml_path : unit -> unit - -val get_compat_version : ?allow_old:bool -> string -> Flags.compat_version |