summaryrefslogtreecommitdiff
path: root/lib/stateid.ml
diff options
context:
space:
mode:
Diffstat (limited to 'lib/stateid.ml')
-rw-r--r--lib/stateid.ml10
1 files changed, 3 insertions, 7 deletions
diff --git a/lib/stateid.ml b/lib/stateid.ml
index a258d505..5485c4bf 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -11,15 +11,11 @@
type t = int
let initial = 1
let dummy = 0
-let fresh, in_range =
+let fresh =
let cur = ref initial in
- (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur)
+ fun () -> incr cur; !cur
let to_string = string_of_int
-let of_int id =
- (* Coqide too to parse ids too, but cannot check if they are valid.
- * Hence we check for validity only if we are an ide slave. *)
- if !Flags.ide_slave then assert (in_range id);
- id
+let of_int id = id
let to_int id = id
let newer_than id1 id2 = id1 > id2