Module Dynlink

Some architectures may have a native ocaml compiler but no native dynlink.cmxa (e.g. ARM). If you still want to build a native coqtop there, you'll need this dummy implementation of Dynlink. Compile it and install with:

ocamlopt -a -o dynlink.cmxa dynlink.ml sudo cp -i dynlink.cmxa `ocamlopt -where`

Then build coq this way: ./configure -natdynlink no && make world

val is_native : bool
type linking_error =
| Undefined_global of string
| Unavailable_primitive of string
| Uninitialized_global of string
type error =
| Not_a_bytecode_file of string
| Inconsistent_import of string
| Unavailable_unit of string
| Unsafe_file
| Linking_error of string * linking_error
| Corrupted_interface of string
| File_not_found of string
| Cannot_open_dll of string
| Inconsistent_implementation of string
exception Error of error
val error_message : error -> string
val loadfile : string -> unit
val loadfile_private : string -> unit
val adapt_filename : 'a -> 'a
val init : unit -> unit
val allow_only : string list -> unit
val prohibit : string list -> unit
val default_available_units : unit -> unit
val allow_unsafe_modules : bool -> unit
val add_interfaces : string list -> string list -> unit
val add_available_units : (string * Stdlib.Digest.t) list -> unit
val clear_available_units : unit -> unit
val digest_interface : string -> string list -> Stdlib.Digest.t