diff options
| author | Pierre-Marie Pédrot | 2018-10-02 08:38:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-02 08:38:04 +0200 |
| commit | 1bde8c0912ed1129e71ffe20299ac89299492ba5 (patch) | |
| tree | 233f39e5a2b34e78f2b157373a307635b0f632f9 /vernac | |
| parent | e53309b2a3c3c1d63b2c5a3cda17765042a9f6c7 (diff) | |
| parent | ef3fa51c12c450781facb61f54f465a77a359f83 (diff) | |
Merge PR #7522: [ocaml] Update required OCaml version to 4.05.0
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 |