diff options
| author | Emilio Jesus Gallego Arias | 2018-05-15 04:25:05 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-09-26 16:44:04 +0200 |
| commit | ef3fa51c12c450781facb61f54f465a77a359f83 (patch) | |
| tree | 583760a05d9530060f6ba9054c408d88fca6dc4a /vernac | |
| parent | f49928874b51458fb67e89618bb350ae2f3529e4 (diff) | |
[ocaml] Update required OCaml version to 4.05.0
Closes #7380. Ubuntu 18.04 and Debian Buster will ship this OCaml
version so it makes sense we bump our dependency to 4.05.0 as we can
use some newer compiler features.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/mltop.ml | 10 | ||||
| -rw-r--r-- | vernac/mltop.mli | 3 |
2 files changed, 4 insertions, 9 deletions
diff --git a/vernac/mltop.ml b/vernac/mltop.ml index d25dea1413..3620e177fe 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -69,9 +69,6 @@ type kind_load = (* Must be always initialized *) let load = ref WithoutTop -(* Are we in a native version of Coq? *) -let is_native = Dynlink.is_native - (* Sets and initializes a toplevel (if any) *) let set_top toplevel = load := WithTop toplevel; @@ -89,7 +86,7 @@ let is_ocaml_top () = |_ -> false (* Tests if we can load ML files *) -let has_dynlink = Coq_config.has_natdynlink || not is_native +let has_dynlink = Coq_config.has_natdynlink || not Sys.(backend_type = Native) (* Runs the toplevel loop of Ocaml *) let ocaml_toploop () = @@ -149,7 +146,7 @@ let dir_ml_use s = | WithTop t -> t.use_file s | _ -> let moreinfo = - if Dynlink.is_native then " Loading ML code works only in bytecode." + if Sys.(backend_type = Native) then " Loading ML code works only in bytecode." else "" in user_err ~hdr:"Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo) @@ -257,7 +254,8 @@ let file_of_name name = str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in if not (Filename.is_relative name) then if Sys.file_exists name then name else fail name - else if is_native then + else if Sys.(backend_type = Native) then + (* XXX: Dynlink.adapt_filename does the same? *) let name = match suffix with | Some ((".cmo"|".cma") as suffix) -> (Filename.chop_suffix name suffix) ^ ".cmxs" diff --git a/vernac/mltop.mli b/vernac/mltop.mli index ed1f9a12d8..3d796aa4aa 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -21,9 +21,6 @@ type toplevel = { (** Sets and initializes a toplevel (if any) *) val set_top : toplevel -> unit -(** Are we in a native version of Coq? *) -val is_native : bool - (** Removes the toplevel (if any) *) val remove : unit -> unit |