1 files changed, 51 insertions, 0 deletions
diff --git a/dev/dynlink.ml b/dev/dynlink.ml
new file mode 100644
index 00000000..810e0ffc
--- /dev/null
+++ b/dev/dynlink.ml
@@ -0,0 +1,51 @@
+
+(** 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
+*)
+
+let is_native = true (* This file will only be given to the native compiler *)
+
+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
+
+let error_message = function
+  | Not_a_bytecode_file s -> "Native dynamic link not supported (module "^s^")"
+  | _ -> "Native dynamic link not supported"
+
+let loadfile : string -> unit = fun s -> raise (Error (Not_a_bytecode_file s))
+let loadfile_private = loadfile
+
+let adapt_filename s = s
+
+let init () = ()
+let allow_only : string list -> unit = fun _ -> ()
+let prohibit : string list -> unit = fun _ -> ()
+let default_available_units : unit -> unit = fun _ -> ()
+let allow_unsafe_modules : bool -> unit = fun _ -> ()
+let add_interfaces : string list -> string list -> unit = fun _ _ -> ()
+let add_available_units : (string * Digest.t) list -> unit = fun _ -> ()
+let clear_available_units : unit -> unit = fun _ -> ()
+let digest_interface : string -> string list -> Digest.t =
+ fun _ _ -> failwith "digest_interface"