Skip to content
Snippets Groups Projects
Unverified Commit 0e5ac043 authored by Emilio Jesus Gallego Arias's avatar Emilio Jesus Gallego Arias
Browse files

[build] Fix a few warnings, adjust flags.

This should make things easier in case we want to use the dev profile.
parent 974fbe89
No related branches found
No related tags found
No related merge requests found
......@@ -50,21 +50,17 @@ type coq_opts = {
external coq_vm_trap : unit -> unit = "coq_vm_trap"
type 'a seq = 'a Seq.t
let feedback_id = ref None
let set_options opt_values =
let open Goptions in
let new_val v old = v in
let new_val v _old = v in
List.iter
(fun (opt, value) -> set_option_value new_val opt value)
opt_values
(**************************************************************************)
(* Low-level, internal Coq initialization *)
(**************************************************************************)
......
......@@ -58,8 +58,8 @@ type search_query =
[@@deriving yojson]
type opaque = Js_of_ocaml.Js.Unsafe.any
let opaque_to_yojson x = `Null
let opaque_of_yojson x = Result.Error "opaque value"
let opaque_to_yojson _x = `Null
let opaque_of_yojson _x = Result.Error "opaque value"
(* Main RPC calls *)
type jscoq_cmd =
......
......@@ -177,7 +177,7 @@ let coq_exn_info exn =
let requires ast =
match ast with
| Vernacexpr.{ expr = VernacRequire (prefix, _export, module_refs)} ->
| Vernacexpr.{ expr = VernacRequire (prefix, _export, module_refs); _ } ->
let prefix_str = match prefix with
| Some ref -> Jslibmng.module_name_of_qualid ref
| _ -> [] in
......
......@@ -223,7 +223,7 @@ let rec last = function
| _ :: t -> last t
let is_intrinsic = function
| "Coq" :: t -> true
| "Coq" :: _ -> true
| _ -> false
let path_to_coqpath ?(implicit=false) ?(unix_prefix=[]) lib_path =
......
(env
(dev (flags :standard -rectypes))
(release (flags :standard -rectypes)))
(release (flags :standard -rectypes -w +27+32)))
(rule
(targets coq-pkgs)
......
......@@ -33,7 +33,7 @@ index 9054507..d21b4f4 100644
if !interrupt then begin interrupt := false; raise Sys.Break end;
incr steps;
if !enable_thread_delay && !steps = 1000 then begin
@@ -79,11 +91,31 @@ let windows_timeout n f x e =
@@ -79,11 +91,32 @@ let windows_timeout n f x e =
let e = Backtrace.add_backtrace e in
Exninfo.iraise e
......@@ -61,6 +61,7 @@ index 9054507..d21b4f4 100644
| _ -> { timeout = windows_timeout }
+*)
+
+let _ = windows_timeout, unix_timeout
+let timeout_fun = { timeout = jscoq_timeout }
let timeout_fun_ref = ref timeout_fun
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment