aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-10-26 17:35:47 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-10-26 17:35:54 +0200
commitff0fea7a07d85342586f65d68e9fdee0ff0c3d74 (patch)
tree5cafa9e671b32acd09e3041139aec781ca9d9b83 /lib
parent4a82de3b5b9d4a1a0830291b5b9a485bf2a16ded (diff)
STM: make ~valid state id non optional from APIs
It used to be Stateid.initial by default. That is indeed a valid state id but very likely not the very best one (that would be the tip of the document).
Diffstat (limited to 'lib')
-rw-r--r--lib/stateid.ml2
-rw-r--r--lib/stateid.mli5
2 files changed, 3 insertions, 4 deletions
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 500581a39..ae25735c5 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -22,7 +22,7 @@ let to_int id = id
let newer_than id1 id2 = id1 > id2
let state_id_info : (t * t) Exninfo.t = Exninfo.make ()
-let add exn ?(valid = initial) id =
+let add exn ~valid id =
Exninfo.add exn state_id_info (valid, id)
let get exn = Exninfo.get exn state_id_info
diff --git a/lib/stateid.mli b/lib/stateid.mli
index cd8fddf0c..1d87a343b 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -26,9 +26,8 @@ val newer_than : t -> t -> bool
(* Attaches to an exception the concerned state id, plus an optional
* state id that is a valid state id before the error.
- * Backtracking to the valid id is safe.
- * The initial_state_id is assumed to be safe. *)
-val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info
+ * Backtracking to the valid id is safe. *)
+val add : Exninfo.info -> valid:t -> t -> Exninfo.info
val get : Exninfo.info -> (t * t) option
type ('a,'b) request = {