diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/flags.ml | 2 | ||||
-rw-r--r-- | lib/flags.mli | 3 | ||||
-rw-r--r-- | lib/stateid.ml | 10 |
3 files changed, 3 insertions, 12 deletions
diff --git a/lib/flags.ml b/lib/flags.ml index 56940f1cf..7e0065beb 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -57,8 +57,6 @@ let in_toplevel = ref false let profile = false -let ide_slave = ref false - let raw_print = ref false let we_are_parsing = ref false diff --git a/lib/flags.mli b/lib/flags.mli index 17776d68a..02d8a3adc 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -52,9 +52,6 @@ val in_toplevel : bool ref val profile : bool -(* -ide_slave: printing will be more verbose, will affect stm caching *) -val ide_slave : bool ref - (* development flag to detect race conditions, it should go away. *) val we_are_parsing : bool ref diff --git a/lib/stateid.ml b/lib/stateid.ml index a258d5052..5485c4bf1 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 |