aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml3
-rw-r--r--lib/flags.mli3
-rw-r--r--lib/stateid.ml8
-rw-r--r--lib/stateid.mli3
4 files changed, 15 insertions, 2 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 4983e40823..3093e52b06 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -68,6 +68,9 @@ let priority_of_string = function
| "low" -> Low
| "high" -> High
| _ -> raise (Invalid_argument "priority_of_string")
+type tac_error_filter = [ `None | `Only of string list | `All ]
+let async_proofs_tac_error_resilience = ref (`Only [ "par" ; "curly" ])
+let async_proofs_cmd_error_resilience = ref true
let async_proofs_is_worker () =
!async_proofs_worker_id <> "master"
diff --git a/lib/flags.mli b/lib/flags.mli
index e13655e4a6..d776815532 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -34,6 +34,9 @@ type priority = Low | High
val async_proofs_worker_priority : priority ref
val string_of_priority : priority -> string
val priority_of_string : string -> priority
+type tac_error_filter = [ `None | `Only of string list | `All ]
+val async_proofs_tac_error_resilience : tac_error_filter ref
+val async_proofs_cmd_error_resilience : bool ref
val debug : bool ref
val in_debugger : bool ref
diff --git a/lib/stateid.ml b/lib/stateid.ml
index c17df2b321..500581a39e 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -29,7 +29,13 @@ let get exn = Exninfo.get exn state_id_info
let equal = Int.equal
let compare = Int.compare
-module Set = Set.Make(struct type t = int let compare = compare end)
+module Self = struct
+ type t = int
+ let compare = compare
+ let equal = equal
+end
+
+module Set = Set.Make(Self)
type ('a,'b) request = {
exn_info : t * t;
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 516ad891ff..cd8fddf0ce 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -11,7 +11,8 @@ type t
val equal : t -> t -> bool
val compare : t -> t -> int
-module Set : Set.S with type elt = t
+module Self : Map.OrderedType with type t = t
+module Set : Set.S with type elt = t and type t = Set.Make(Self).t
val initial : t
val dummy : t