Modulification and removing of structural equality in Stateid.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16705 85f007b7-540e-0410-9357-904b9bb8a0f7

16 files changed, 153 insertions, 154 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 534dd504d..1ca949b52 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -19,13 +19,13 @@ module SentenceId : sig
     stop : GText.mark;
     mutable flags : flag list;
     edit_id : int;
-    mutable state_id : Stateid.state_id option;
+    mutable state_id : Stateid.t option;
   }
 
   val mk_sentence :
     start:GText.mark -> stop:GText.mark -> flag list -> sentence
 
-  val assign_state_id : sentence -> Stateid.state_id -> unit
+  val assign_state_id : sentence -> Stateid.t -> unit
   val set_flags : sentence -> flag list -> unit
   val add_flag : sentence -> flag -> unit
   val remove_flag : sentence -> flag -> unit
@@ -39,7 +39,7 @@ end = struct
     stop : GText.mark;
     mutable flags : flag list;
     edit_id : int;
-    mutable state_id : Stateid.state_id option;
+    mutable state_id : Stateid.t option;
   }
 
   let id = ref 0
@@ -54,7 +54,7 @@ end = struct
 
   let assign_state_id s id =
     assert(s.state_id = None);
-    assert(id <> Stateid.dummy_state_id);
+    assert(id <> Stateid.dummy);
     s.state_id <- Some id
   let set_flags s f = s.flags <- f
   let add_flag s f = s.flags <- CList.add_set f s.flags
@@ -102,7 +102,7 @@ object(self)
 
   val cmd_stack = Searchstack.create ()
 
-  val mutable initial_state = Stateid.initial_state_id
+  val mutable initial_state = Stateid.initial
 
   val feedbacks : feedback Queue.t = Queue.create ()
   val feedback_timer = Ideutils.mktimer ()
@@ -219,7 +219,7 @@ object(self)
   method private is_dummy_id id =
     match id with
     | Edit 0 -> true
-    | State id when id = Stateid.dummy_state_id -> true
+    | State id when Stateid.equal id Stateid.dummy -> true
     | _ -> false
 
   method private enqueue_feedback msg =
@@ -240,8 +240,8 @@ object(self)
         try Some (Searchstack.find finder () cmd_stack)
         with Not_found -> None in
       let log s sentence =
-        Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.string_of_state_id
-          (Option.default Stateid.dummy_state_id sentence.state_id)) in
+        Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string
+          (Option.default Stateid.dummy sentence.state_id)) in
       begin match msg.content, sentence with
       | AddedAxiom, Some sentence ->
           log "AddedAxiom" sentence;
diff --git a/ide/wg_Command.mli b/ide/wg_Command.mli
index 1c5a1e424..2245befe7 100644
--- a/ide/wg_Command.mli
+++ b/ide/wg_Command.mli
@@ -7,9 +7,9 @@
 (************************************************************************)
 
 class command_window : Coq.coqtop ->
-    mark_as_broken:(Stateid.state_id list -> unit) ->
-    mark_as_processed:(Stateid.state_id list -> unit) ->
-    cur_state:(unit -> Stateid.state_id) ->
+    mark_as_broken:(Stateid.t list -> unit) ->
+    mark_as_processed:(Stateid.t list -> unit) ->
+    cur_state:(unit -> Stateid.t) ->
   object
     method new_command : ?command:string -> ?term:string -> unit -> unit
     method frame : GBin.frame
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 30124e5d0..97b038f5c 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -9,7 +9,6 @@
 open Loc
 open Pp
 open Util
-open Stateid
 open Names
 open Tacexpr
 open Misctypes
@@ -220,7 +219,7 @@ type bullet =
 type 'a stm_vernac =
   | JoinDocument
   | Finish
-  | Observe of Stateid.state_id
+  | Observe of Stateid.t
   | Command of 'a (* An out of flow command not to be recorded by Stm *)
   | PGLast of 'a (* To ease the life of PG *)
 
@@ -436,8 +435,8 @@ and vernac_part_of_script = bool
 and vernac_control =
   | VtFinish
   | VtJoinDocument
-  | VtObserve of state_id
-  | VtBack of state_id
+  | VtObserve of Stateid.t
+  | VtBack of Stateid.t
 type vernac_when =
   | VtNow
   | VtLater
diff --git a/lib/interface.mli b/lib/interface.mli
index 274dbbb77..560d80d83 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -117,7 +117,7 @@ type message = {
 
 (** Coq "semantic" infos obtained during parsing/execution *)
 type edit_id = int
-type state_id = Stateid.state_id
+type state_id = Stateid.t
 type edit_or_state_id = Edit of edit_id | State of state_id
 
 type feedback_content =
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 6636c24f0..c6eaa4eda 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -355,9 +355,9 @@ let to_edit_id = function
   | _ -> raise Marshal_error
 
 let of_state_id id =
-  try Stateid.of_state_id id with Invalid_argument _ -> raise Marshal_error
+  try Stateid.to_xml id with Invalid_argument _ -> raise Marshal_error
 let to_state_id xml =
-  try Stateid.to_state_id xml with Invalid_argument _ -> raise Marshal_error
+  try Stateid.of_xml xml with Invalid_argument _ -> raise Marshal_error
 
 let of_edit_or_state_id = function
   | Interface.Edit id -> ["object","edit"], of_edit_id id
@@ -727,7 +727,7 @@ let pr_call = function
     let raw = if r then "RAW" else "" in
     let verb = if b then "" else "SILENT" in
     "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]"
-  | Backto i -> "BACKTO "^(Stateid.string_of_state_id i)
+  | Backto i -> "BACKTO "^(Stateid.to_string i)
   | Goal _ -> "GOALS"
   | Evars _ -> "EVARS"
   | Hints _ -> "HINTS"
@@ -744,9 +744,9 @@ let pr_call = function
   | Init _ -> "INIT"
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
-  | Fail (id,None,str) -> "FAIL "^Stateid.string_of_state_id id^" ["^str^"]"
+  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]"
   | Fail (id,Some(i,j),str) ->
-      "FAIL "^Stateid.string_of_state_id id^
+      "FAIL "^Stateid.to_string id^
         " ("^string_of_int i^","^string_of_int j^")["^str^"]"
 let pr_value v = pr_value_gen (fun _ -> "FIXME") v
 let pr_full_value call value =
diff --git a/lib/stateid.ml b/lib/stateid.ml
index 3abd80cfb..1eac4bf3f 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -8,18 +8,18 @@
 
 open Xml_datatype
 
-type state_id = int
-let initial_state_id = 1
-let dummy_state_id = 0
-let fresh_state_id, in_range =
-  let cur = ref initial_state_id in
+type t = int
+let initial = 1
+let dummy = 0
+let fresh, in_range =
+  let cur = ref initial in
   (fun () -> incr cur; !cur), (fun id -> id >= 0 && id <= !cur)
-let string_of_state_id = string_of_int
-let state_id_of_int id = assert(in_range id); id
-let int_of_state_id id = id
+let to_string = string_of_int
+let of_int id = assert(in_range id); id
+let to_int id = id
 let newer_than id1 id2 = id1 > id2
 
-let to_state_id = function
+let of_xml = function
   | Element ("state_id",["val",i],[]) ->
       let id = int_of_string i in
       (* Coqide too to parse ids too, but cannot check if they are valid.
@@ -27,11 +27,12 @@ let to_state_id = function
       if !Flags.ide_slave then assert(in_range id);
       id
   | _ -> raise (Invalid_argument "to_state_id")
-let of_state_id i = Element ("state_id",["val",string_of_int i],[])
+let to_xml i = Element ("state_id",["val",string_of_int i],[])
 
-let state_id_info : (state_id * state_id) Exninfo.t = Exninfo.make ()
-let add_state_id exn ?(valid = initial_state_id) id =
+let state_id_info : (t * t) Exninfo.t = Exninfo.make ()
+let add exn ?(valid = initial) id =
   Exninfo.add exn state_id_info (valid, id)
-let get_state_id exn = Exninfo.get exn state_id_info
+let get exn = Exninfo.get exn state_id_info
 
-module StateidOrderedType = struct type t = state_id let compare = compare end
+let equal = Int.equal
+let compare = Int.compare
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 978f12691..27b083efd 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -8,24 +8,26 @@
 
 open Xml_datatype
 
-type state_id
-val initial_state_id : state_id
-val dummy_state_id : state_id
-val fresh_state_id : unit -> state_id
-val string_of_state_id : state_id -> string
-val state_id_of_int : int -> state_id
-val int_of_state_id : state_id -> int
-val newer_than : state_id -> state_id -> bool
+type t
+
+val equal : t -> t -> bool
+val compare : t -> t -> int
+
+val initial : t
+val dummy : t
+val fresh : unit -> t
+val to_string : t -> string
+val of_int : int -> t
+val to_int : t -> int
+val newer_than : t -> t -> bool
 
 (* XML marshalling *)
-val of_state_id : state_id -> xml
-val to_state_id : xml -> state_id
+val to_xml : t -> xml
+val of_xml : xml -> t
 
 (* 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_state_id : exn -> ?valid:state_id -> state_id -> exn
-val get_state_id : exn -> (state_id * state_id) option
-
-module StateidOrderedType : Map.OrderedType with type t = state_id
+val add : exn -> ?valid:t -> t -> exn
+val get : exn -> (t * t) option
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 33f375a83..fe8e0787c 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -81,7 +81,7 @@ GEXTEND Gram
       | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument
       | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish
       | IDENT "Stm"; IDENT "Observe"; id = INT; "." ->
-          VernacStm (Observe (Stateid.state_id_of_int (int_of_string id)))
+          VernacStm (Observe (Stateid.of_int (int_of_string id)))
       | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v)
       | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v)
 
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index b5277b62e..06d095818 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -480,7 +480,7 @@ let rec pr_vernac = function
   | VernacStm JoinDocument -> str"Stm JoinDocument"
   | VernacStm Finish -> str"Stm Finish"
   | VernacStm (Observe id) ->
-      str"Stm Observe " ++ str(Stateid.string_of_state_id id)
+      str"Stm Observe " ++ str(Stateid.to_string id)
   | VernacStm (Command v) -> str"Stm Command " ++ pr_vernac v
   | VernacStm (PGLast v) -> str"Stm PGLast " ++ pr_vernac v
 
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index 5bfa377f0..19a82d6ea 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -46,7 +46,7 @@ let store_id = function
 let rec erase_ids n =
   if n = 0 then
     match !ids with
-    | [] -> Stateid.initial_state_id
+    | [] -> Stateid.initial
     | x :: _ -> x
   else match !ids with
     | id :: rest -> ids := rest; erase_ids (n-1)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 65b446ca0..660bd4f3e 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -125,7 +125,7 @@ let interp (id,raw,verbosely,s) =
 
 let backto id =
   Vernac.eval_expr (Loc.ghost,
-    VernacStm (Command (VernacBackTo (Stateid.int_of_state_id id))))
+    VernacStm (Command (VernacBackTo (Stateid.to_int id))))
 
 (** Goal display *)
 
@@ -292,7 +292,7 @@ let about () = {
 }
 
 let handle_exn e =
-  let dummy = Stateid.dummy_state_id in
+  let dummy = Stateid.dummy in
   let loc_of e = match Loc.get_loc e with
     | Some loc when not (Loc.is_ghost loc) -> Some (Loc.unloc loc)
     | _ -> None in
@@ -301,7 +301,7 @@ let handle_exn e =
   | Errors.Drop -> dummy, None, "Drop is not allowed by coqide!"
   | Errors.Quit -> dummy, None, "Quit is not allowed by coqide!"
   | e ->
-      match Stateid.get_state_id e with
+      match Stateid.get e with
       | Some (valid, _) -> valid, loc_of e, mk_msg e
       | None -> dummy, loc_of e, mk_msg e
 
diff --git a/toplevel/stm.ml b/toplevel/stm.ml
index eb83c81f6..db0843c82 100644
--- a/toplevel/stm.ml
+++ b/toplevel/stm.ml
@@ -8,7 +8,6 @@
 
 let prerr_endline s = if !Flags.debug then prerr_endline s else ()
 
-open Stateid
 open Vernacexpr
 open Errors
 open Pp
@@ -39,7 +38,7 @@ let interp ?proof id (verbosely, loc, expr) =
 type ast = bool * Loc.t * vernac_expr
 let pr_ast (_, _, v) = pr_vernac v
 
-module Vcs_ = Vcs.Make(StateidOrderedType)
+module Vcs_ = Vcs.Make(Stateid)
 
 type branch_type = [ `Master | `Proof of string * int ]
 type cmd_t = ast * Id.t list
@@ -47,7 +46,7 @@ type fork_t = ast * Vcs_.Branch.t * Id.t list
 type qed_t =
   ast * vernac_qed_type * (Vcs_.Branch.t * branch_type Vcs_.branch_info)
 type seff_t = ast option
-type alias_t = state_id
+type alias_t = Stateid.t
 type transaction =
   | Cmd    of cmd_t
   | Fork   of fork_t
@@ -58,11 +57,11 @@ type transaction =
 type step =
   [ `Cmd    of cmd_t
   | `Fork   of fork_t
-  | `Qed    of qed_t * state_id
+  | `Qed    of qed_t * Stateid.t
   (* TODO : is the state id carried by `Ast relevant? *)
-  | `Sideff of [ `Ast of ast * state_id | `Id of state_id ]
+  | `Sideff of [ `Ast of ast * Stateid.t | `Id of Stateid.t ]
   | `Alias  of alias_t ]
-type visit = { step : step; next : state_id }
+type visit = { step : step; next : Stateid.t }
 
 type state = States.state * Proof_global.state
 type state_info = { (* Make private *)
@@ -90,7 +89,7 @@ end = struct (* {{{ *)
 
   let find_proof_at_depth vcs pl =
     try List.find (function
-          | _, { Vcs_.kind = `Proof(m, n) } -> n = pl
+          | _, { Vcs_.kind = `Proof(m, n) } -> Int.equal n pl
           | _ -> false)
         (List.map (fun h -> h, Vcs_.get_branch vcs h) (Vcs_.branches vcs))
     with Not_found -> failwith "find_proof_at_depth"
@@ -101,7 +100,7 @@ end (* }}} *)
 module VCS : sig
 
   module Branch : (module type of Vcs_.Branch with type t = Vcs_.Branch.t)
-  type id = state_id
+  type id = Stateid.t
   type 'branch_type branch_info = 'branch_type Vcs_.branch_info = {
     kind : [> `Master] as 'branch_type;
     root : id;
@@ -152,7 +151,7 @@ end = struct (* {{{ *)
 
   include Vcs_
 
-  module StateidSet = Set.Make(StateidOrderedType)
+  module StateidSet = Set.Make(Stateid)
   open Printf
 
   let print_dag vcs () = (* {{{ *)
@@ -165,7 +164,7 @@ end = struct (* {{{ *)
             (try string_of_ppcmds (pr_ast t) with _ -> "ERR")
       | Sideff None -> "EnvChange"
       | Noop -> " "
-      | Alias id -> sprintf "Alias(%s)" (string_of_state_id id)
+      | Alias id -> sprintf "Alias(%s)" (Stateid.to_string id)
       | Qed (a,_,_) -> string_of_ppcmds (pr_ast a) in
     let is_green id = 
       match get_info vcs id with
@@ -173,7 +172,7 @@ end = struct (* {{{ *)
       | _ -> false in
     let is_red id =
       match get_info vcs id with
-      | Some s -> s.n_reached = ~-1
+      | Some s -> Int.equal s.n_reached ~-1
       | _ -> false in
     let head = current_branch vcs in
     let heads =
@@ -189,7 +188,7 @@ end = struct (* {{{ *)
     let fname_dot, fname_ps =
       let f = "/tmp/" ^ Filename.basename fname in
       f ^ ".dot", f ^ ".pdf" in
-    let node id = "s" ^ string_of_state_id id in
+    let node id = "s" ^ Stateid.to_string id in
     let edge tr =
       sprintf "<<FONT POINT-SIZE=\"12\" FACE=\"sans\">%s</FONT>>"
         (quote (string_of_transaction tr)) in
@@ -199,7 +198,7 @@ end = struct (* {{{ *)
       match get_info vcs id with
       | None -> ""
       | Some info ->
-          sprintf "<<FONT POINT-SIZE=\"12\">%s</FONT>" (string_of_state_id id) ^
+          sprintf "<<FONT POINT-SIZE=\"12\">%s</FONT>" (Stateid.to_string id) ^
           sprintf " <FONT POINT-SIZE=\"11\">r:%d g:%d</FONT>>"
             info.n_reached info.n_goals in
     let color id =
@@ -229,7 +228,7 @@ end = struct (* {{{ *)
        fprintf oc "color=blue; }\n"
     ) clus;
     List.iteri (fun i (b,id) ->
-      let shape = if head = b then "box3d" else "box" in
+      let shape = if Branch.equal head b then "box3d" else "box" in
       fprintf oc "b%d -> %s;\n" i (node id);
       fprintf oc "b%d [shape=%s,label=\"%s\"];\n" i shape
         (Branch.to_string b);
@@ -242,7 +241,7 @@ end = struct (* {{{ *)
   
   exception Expired
   type vcs = (branch_type, transaction, state_info) t
-  let vcs : vcs ref = ref (empty dummy_state_id)
+  let vcs : vcs ref = ref (empty Stateid.dummy)
 
   let init id =
     vcs := empty id;
@@ -256,7 +255,7 @@ end = struct (* {{{ *)
   let get_branch head = get_branch !vcs head
   let get_branch_pos head = (get_branch head).pos
   let new_node () =
-    let id = Stateid.fresh_state_id () in
+    let id = Stateid.fresh () in
     vcs := set_info !vcs id (default_info ());
     id
   let merge id ~ours ?into branch =
@@ -301,7 +300,7 @@ end = struct (* {{{ *)
       checkout b;
       let id = new_node () in
       merge id ~ours:(Sideff t) ~into:b Branch.master)
-    (List.filter ((<>) Branch.master) (branches ()))
+    (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
   
   let visit id =
     try
@@ -315,26 +314,26 @@ end = struct (* {{{ *)
       | [p, Noop; n, Sideff None]-> { step = `Sideff (`Id p); next = n }
       | [n, Sideff (Some x); p, Noop]
       | [p, Noop; n, Sideff (Some x)]-> { step = `Sideff(`Ast (x,p)); next = n }
-      | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,dummy_state_id)); next=n}
-      | _ -> anomaly (str ("Malformed VCS at node "^string_of_state_id id))
+      | [n, Sideff (Some x)]-> {step = `Sideff(`Ast (x,Stateid.dummy)); next=n}
+      | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id))
     with Not_found -> raise Expired
 
   let slice ~start ~stop ~purify =
     let l =
       let rec aux id =
-        if id = stop then [] else
+        if Stateid.equal id stop then [] else
         match visit id with
         | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n
         | { next = n; step = `Alias x } -> (id,Alias x) :: aux n
         | { next = n; step = `Sideff (`Ast (x,_)) } ->
              (id,Sideff (Some x)) :: aux n
-        | _ -> anomaly(str("Cannot slice from "^ string_of_state_id start ^
-                           " to "^string_of_state_id stop))
+        | _ -> anomaly(str("Cannot slice from "^ Stateid.to_string start ^
+                           " to "^Stateid.to_string stop))
       in aux start in
     let v = Vcs_.empty stop in
     let info = get_info stop in
     (* Stm should have reached the beginning of proof *)
-    assert(info.state <> None);
+    assert (not (Option.is_empty info.state));
     (* This may be expensive *)
     let info = { info with state = Some (purify (Option.get info.state)) } in
     let v = Vcs_.set_info v stop info in
@@ -367,7 +366,7 @@ end = struct (* {{{ *)
 
     let get_last_job () =
       Mutex.lock m;
-      while !job = None do Condition.wait c m; done;
+      while Option.is_empty !job do Condition.wait c m; done;
       match !job with
       | None -> assert false
       | Some x -> job := None; Mutex.unlock m; x
@@ -377,7 +376,7 @@ end = struct (* {{{ *)
 
     let command job =
       set_last_job job;
-      if !worker = None then worker := Some (Thread.create run_command ())
+      if Option.is_empty !worker then worker := Some (Thread.create run_command ())
 
   end (* }}} *)
 
@@ -398,12 +397,12 @@ module State : sig
 
       Warning: an optimization requires that state modifying functions
       are always executed using this wrapper. *)
-  val define : ?cache:bool -> (unit -> unit) -> state_id -> unit
+  val define : ?cache:bool -> (unit -> unit) -> Stateid.t -> unit
 
-  val install_cached : state_id -> unit
-  val is_cached : state_id -> bool
+  val install_cached : Stateid.t -> unit
+  val is_cached : Stateid.t -> bool
 
-  val exn_on : state_id -> ?valid:state_id -> exn -> exn
+  val exn_on : Stateid.t -> ?valid:Stateid.t -> exn -> exn
 
   (* TODO: rename *)
   (* projects a state so that it can be marshalled and its content is
@@ -412,9 +411,9 @@ module State : sig
 
 end = struct (* {{{ *)
 
-  (* cur_id holds dummy_state_id in case the last attempt to define a state
+  (* cur_id holds Stateid.dummy in case the last attempt to define a state
    * failed, so the global state may contain garbage *)
-  let cur_id = ref dummy_state_id
+  let cur_id = ref Stateid.dummy
 
   (* helpers *)
   let freeze_global_state marshallable =
@@ -435,13 +434,13 @@ end = struct (* {{{ *)
       ) s
 
   let is_cached id =
-    id = !cur_id ||
+    Stateid.equal id !cur_id ||
     match VCS.get_info id with
     | { state = Some _ } -> true
     | _ -> false
 
   let install_cached id =
-    if id = !cur_id then () else (* optimization *)
+    if Stateid.equal id !cur_id then () else (* optimization *)
     let s =
       match VCS.get_info id with
       | { state = Some s } -> s
@@ -454,14 +453,14 @@ end = struct (* {{{ *)
     let loc = Option.default Loc.ghost (Loc.get_loc e) in
     let msg = string_of_ppcmds (print e) in
     Pp.feedback ~state_id:id (Interface.ErrorMsg (loc, msg));
-    Stateid.add_state_id e ?valid id
+    Stateid.add e ?valid id
 
   let define ?(cache=false) f id =
     if is_cached id then
-      anomaly (str"defining state "++str(string_of_state_id id)++str" twice");
+      anomaly (str"defining state "++str(Stateid.to_string id)++str" twice");
     try
       prerr_endline ("defining " ^
-        string_of_state_id id ^ " (cache=" ^string_of_bool cache^")");
+        Stateid.to_string id ^ " (cache=" ^string_of_bool cache^")");
       f ();
       if cache then freeze `No id;
       cur_id := id;
@@ -472,9 +471,9 @@ end = struct (* {{{ *)
     with e ->
       let e = Errors.push e in
       let good_id = !cur_id in
-      cur_id := dummy_state_id;
+      cur_id := Stateid.dummy;
       VCS.reached id false;
-      match Stateid.get_state_id e with
+      match Stateid.get e with
       | Some _ -> raise e
       | None -> raise (exn_on id ~valid:good_id e)
 
@@ -487,7 +486,7 @@ module Slaves : sig
 
   (* (eventually) remote calls *)
   val build_proof :
-    exn_info:(state_id * state_id) -> start:state_id -> stop:state_id ->
+    exn_info:(Stateid.t * Stateid.t) -> start:Stateid.t -> stop:Stateid.t ->
       Entries.proof_output list Future.computation
   
   (* initialize the whole machinery (optional) *)
@@ -498,7 +497,7 @@ module Slaves : sig
   val slave_init_stdout : unit -> unit
 
   (* to disentangle modules *)
-  val set_reach_known_state : (cache:bool -> state_id -> unit) -> unit
+  val set_reach_known_state : (cache:bool -> Stateid.t -> unit) -> unit
 
 
 end = struct (* {{{ *)
@@ -542,7 +541,7 @@ end = struct (* {{{ *)
   
     let slave_manager = ref (None : Thread.t option)
     
-    let is_empty () = !slave_manager = None
+    let is_empty () = Option.is_empty !slave_manager
 
     let respawn () =
       let c2s_r, c2s_w = Unix.pipe () in
@@ -565,7 +564,7 @@ end = struct (* {{{ *)
   let reach_known_state = ref (fun ~cache id -> ())
   let set_reach_known_state f = reach_known_state := f
 
-  type request = ReqBuildProof of (state_id * state_id) * state_id * VCS.vcs
+  type request = ReqBuildProof of (Stateid.t * Stateid.t) * Stateid.t * VCS.vcs
   type response =
     | RespBuiltProof of Entries.proof_output list 
     | RespError of std_ppcmds
@@ -574,15 +573,15 @@ end = struct (* {{{ *)
     | RespBuiltProof _ -> "Sucess"
     | RespError _ -> "Error"
     | RespFeedback { Interface.id = Interface.State id } ->
-        "Feedback on " ^ string_of_state_id id
+        "Feedback on " ^ Stateid.to_string id
     | RespFeedback _ -> assert false
  
   type task =
-    | TaskBuildProof of (state_id * state_id) * state_id * state_id *
+    | TaskBuildProof of (Stateid.t * Stateid.t) * Stateid.t * Stateid.t *
         (Entries.proof_output list Future.value -> unit)
   let pr_task = function
     | TaskBuildProof(_,bop,eop,_) ->
-        "TaskBuilProof("^string_of_state_id bop^","^string_of_state_id eop^")"
+        "TaskBuilProof("^Stateid.to_string bop^","^Stateid.to_string eop^")"
 
   let request_of_task task =
     match task with
@@ -719,7 +718,7 @@ end (* }}} *)
 (* Runs all transactions needed to reach a state *)
 module Reach : sig
 
-  val known_state : cache:bool -> state_id -> unit
+  val known_state : cache:bool -> Stateid.t -> unit
 
 end = struct (* {{{ *)
 
@@ -739,10 +738,10 @@ let collect_proof cur hd id =
     | _, `Fork(_,_,_::_::_)->
         `NotOptimizable `MutualProofs (* TODO: enderstand where we need that *)
     | Some (parent, (_,_,VernacProof(_,Some _) as v)), `Fork (_, hd', _) ->
-        assert( hd = hd' );
+        assert (VCS.Branch.equal hd hd');
         `Optimizable (parent, Some v, accn)
     | Some (parent, _), `Fork (_, hd', _) ->
-        assert( hd = hd' );
+        assert (VCS.Branch.equal hd hd');
         `MaybeOptimizable (parent, accn)
     | _, `Sideff se -> collect None (id::accn) view.next
     | _ -> `NotOptimizable `Unknown in
@@ -760,13 +759,13 @@ let known_state ~cache id =
   let inject_non_pstate (s,l) = Summary.unfreeze_summary s; Lib.unfreeze l in
 
   let rec pure_cherry_pick_non_pstate id = Future.purify (fun id ->
-    prerr_endline ("cherry-pick non pstate " ^ string_of_state_id id);
+    prerr_endline ("cherry-pick non pstate " ^ Stateid.to_string id);
     reach id;
     cherry_pick_non_pstate ()) id
 
   (* traverses the dag backward from nodes being already calculated *)
   and reach ?(cache=cache) id =
-    prerr_endline ("reaching: " ^ string_of_state_id id);
+    prerr_endline ("reaching: " ^ Stateid.to_string id);
     if State.is_cached id then begin
       State.install_cached id;
       feedback ~state_id:id Interface.Processed;
@@ -785,7 +784,7 @@ let known_state ~cache id =
            let rec aux = function
            | `Optimizable (start, proof_using_ast, nodes) ->
                (fun () ->
-                 prerr_endline ("Optimizable " ^ string_of_state_id id);
+                 prerr_endline ("Optimizable " ^ Stateid.to_string id);
                  VCS.create_cluster nodes;
                  begin match keep with
                  | VtKeep ->
@@ -802,11 +801,11 @@ let known_state ~cache id =
                      interp id x
                  end;
                  Proof_global.discard_all ())
-           | `NotOptimizable `Immediate -> assert (view.next = eop);
+           | `NotOptimizable `Immediate -> assert (Stateid.equal view.next eop);
                (fun () -> reach eop; interp id x; Proof_global.discard_all ())
            | `NotOptimizable _ ->
                (fun () ->
-                 prerr_endline ("NotOptimizable " ^ string_of_state_id id);
+                 prerr_endline ("NotOptimizable " ^ Stateid.to_string id);
                  reach eop;
                  begin match keep with
                  | VtKeep ->
@@ -820,10 +819,10 @@ let known_state ~cache id =
                  Proof_global.discard_all ())
            | `MaybeOptimizable (start, nodes) ->
                (fun () ->
-                 prerr_endline ("MaybeOptimizable " ^ string_of_state_id id);
+                 prerr_endline ("MaybeOptimizable " ^ Stateid.to_string id);
                  reach ~cache:true start;
                  (* no sections and no modules *)
-                 if Environ.named_context (Global.env ()) = [] &&
+                 if List.is_empty (Environ.named_context (Global.env ())) &&
                     Safe_typing.is_curmod_library (Global.safe_env ()) then
                    aux (`Optimizable (start, None, nodes)) ()
                  else
@@ -840,7 +839,7 @@ let known_state ~cache id =
            cache
     in
     State.define ~cache:cache_step step id;
-    prerr_endline ("reached: "^ string_of_state_id id) in
+    prerr_endline ("reached: "^ Stateid.to_string id) in
   reach id
 
 end (* }}} *)
@@ -850,11 +849,11 @@ let _ = Slaves.set_reach_known_state Reach.known_state
 module Backtrack : sig
 
   val record : unit -> unit
-  val backto : state_id -> unit
-  val cur : unit -> state_id
+  val backto : Stateid.t -> unit
+  val cur : unit -> Stateid.t
 
   (* we could navigate the dag, but this ways easy *)
-  val branches_of : state_id -> VCS.Branch.t list
+  val branches_of : Stateid.t -> VCS.Branch.t list
 
   (* To be installed during initialization *)
   val undo_vernac_classifier : vernac_expr -> vernac_classification
@@ -864,7 +863,7 @@ end = struct (* {{{ *)
   module S  = Searchstack
 
   type hystory_elt = {
-    id : state_id ;
+    id : Stateid.t ;
     vcs : VCS.vcs;
     label : Names.Id.t list; (* To implement a limited form of reset *)
   }
@@ -881,7 +880,7 @@ end = struct (* {{{ *)
       id = id;
       vcs = VCS.backup ();
       label =
-        if id = initial_state_id || id = dummy_state_id then [] else 
+        if Stateid.equal id Stateid.initial || Stateid.equal id Stateid.dummy then [] else 
         match VCS.visit id with
         | { step = `Fork (_,_,l) } -> l
         | { step = `Cmd (_,l) } -> l
@@ -892,23 +891,23 @@ end = struct (* {{{ *)
     assert(not (S.is_empty history));
     let rec pop_until_oid () =
       let id = (S.top history).id in
-      if id = initial_state_id || id = oid then ()
+      if Stateid.equal id Stateid.initial || Stateid.equal id oid then ()
       else begin ignore (S.pop history); pop_until_oid (); end in
     pop_until_oid ();
     let backup = S.top history in
     VCS.restore backup.vcs;
-    if backup.id <> oid then anomaly (str "Backto an unknown state")
+    if not (Stateid.equal backup.id oid) then anomaly (str "Backto an unknown state")
 
   let branches_of id =
     try
       let s = S.find (fun n s ->
-        if s.id = id then `Stop s else `Cont ()) () history in
+        if Stateid.equal s.id id then `Stop s else `Cont ()) () history in
       Vcs_.branches s.vcs
     with Not_found -> assert false
  
   let undo_vernac_classifier = function
     | VernacResetInitial ->
-        VtStm (VtBack initial_state_id, true), VtNow
+        VtStm (VtBack Stateid.initial, true), VtNow
     | VernacResetName (_,name) ->
         msg_warning
           (str"Reset not implemented for automatically generated constants");
@@ -922,11 +921,11 @@ end = struct (* {{{ *)
           VtStm (VtBack (S.top history).id, true), VtNow)
     | VernacBack n ->
         let s = S.find (fun n s ->
-          if n = 0 then `Stop s else `Cont (n-1)) n history in
+          if Int.equal n 0 then `Stop s else `Cont (n-1)) n history in
         VtStm (VtBack s.id, true), VtNow
     | VernacUndo n ->
         let s = S.find (fun n s ->
-          if n = 0 then `Stop s else `Cont (n-1)) n history in
+          if Int.equal n 0 then `Stop s else `Cont (n-1)) n history in
         VtStm (VtBack s.id, true), VtLater
     | VernacUndoTo _
     | VernacRestart as e ->
@@ -938,16 +937,16 @@ end = struct (* {{{ *)
           if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
           0 history in
         let s = S.find (fun n s ->
-          if n = 0 then `Stop s else `Cont (n-1)) (n-m-1) history in
+          if Int.equal n 0 then `Stop s else `Cont (n-1)) (n-m-1) history in
         VtStm (VtBack s.id, true), VtLater
     | VernacAbortAll ->
         let s = S.find (fun () s ->
-          if List.length (Vcs_.branches s.vcs) = 1 then `Stop s else `Cont ())
+          match Vcs_.branches s.vcs with [_] -> `Stop s | _ -> `Cont ())
           () history in
         VtStm (VtBack s.id, true), VtLater
     | VernacBacktrack (id,_,_)
     | VernacBackTo id ->
-        VtStm (VtBack (Stateid.state_id_of_int id), true), VtNow
+        VtStm (VtBack (Stateid.of_int id), true), VtNow
     | _ -> VtUnknown, VtNow
 
 end (* }}} *)
@@ -956,11 +955,11 @@ let slave_main_loop () = Slaves.slave_main_loop ()
 let slave_init_stdout () = Slaves.slave_init_stdout ()
 
 let init () =
-  VCS.init initial_state_id;
+  VCS.init Stateid.initial;
   set_undo_classifier Backtrack.undo_vernac_classifier;
-  State.define ~cache:true (fun () -> ()) initial_state_id;
+  State.define ~cache:true (fun () -> ()) Stateid.initial;
   Backtrack.record ();
-  if !Flags.coq_slave_mode = 0 then Slaves.init ()
+  if Int.equal !Flags.coq_slave_mode 0 then Slaves.init ()
 
 let observe id =
   let vcs = VCS.backup () in
@@ -979,7 +978,7 @@ let finish () =
 
 let join_aborted_proofs () =
   let rec aux id =
-    if id = initial_state_id then () else
+    if Stateid.equal id Stateid.initial then () else
     let view = VCS.visit id in
     match view.step with
     | `Qed ((_,VtDrop,_),eop) ->
@@ -1000,13 +999,13 @@ let join () =
 
 let merge_proof_branch x keep branch =
   if VCS.Branch.equal branch VCS.Branch.master then
-    raise(State.exn_on dummy_state_id Proof_global.NoCurrentProof);
+    raise(State.exn_on Stateid.dummy Proof_global.NoCurrentProof);
   let info = VCS.get_branch branch in
   VCS.checkout VCS.Branch.master;
   let id = VCS.new_node () in
   VCS.merge id ~ours:(Qed (x,keep,(branch, info))) branch;
   VCS.delete_branch branch;
-  if keep = VtKeep then VCS.propagate_sideff None
+  if keep == VtKeep then VCS.propagate_sideff None
 
 let process_transaction verbosely (loc, expr) =
   let warn_if_pos a b =
@@ -1038,9 +1037,9 @@ let process_transaction verbosely (loc, expr) =
             (VCS.branches ());
           VCS.checkout_shallowest_proof_branch ();
           VCS.commit id (Alias oid);
-          Backtrack.record (); if w = VtNow then finish ()
+          Backtrack.record (); if w == VtNow then finish ()
       | VtStm (VtBack id, false), VtNow ->
-          prerr_endline ("undo to state " ^ string_of_state_id id);
+          prerr_endline ("undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
           Reach.known_state ~cache:(interactive ()) id;
@@ -1050,14 +1049,14 @@ let process_transaction verbosely (loc, expr) =
       (* Query *)
       | VtQuery false, VtNow ->
           finish ();
-          (try Future.purify (interp dummy_state_id) (true,loc,expr)
+          (try Future.purify (interp Stateid.dummy) (true,loc,expr)
            with e when Errors.noncritical e ->
              let e = Errors.push e in
-             raise(State.exn_on dummy_state_id e))
+             raise(State.exn_on Stateid.dummy e))
       | VtQuery true, w ->
           let id = VCS.new_node () in
           VCS.commit id (Cmd (x,[]));
-          Backtrack.record (); if w = VtNow then finish ()
+          Backtrack.record (); if w == VtNow then finish ()
       | VtQuery false, VtLater ->
           anomaly(str"classifier: VtQuery + VtLater must imply part_of_script")
 
@@ -1069,15 +1068,15 @@ let process_transaction verbosely (loc, expr) =
           VCS.commit id (Fork (x, bname, names));
           VCS.branch bname (`Proof (mode, VCS.proof_nesting () + 1));
           Proof_global.activate_proof_mode mode;
-          Backtrack.record (); if w = VtNow then finish ()
+          Backtrack.record (); if w == VtNow then finish ()
       | VtProofStep, w ->
           let id = VCS.new_node () in
           VCS.commit id (Cmd (x,[]));
-          Backtrack.record (); if w = VtNow then finish ()
+          Backtrack.record (); if w == VtNow then finish ()
       | VtQed keep, w ->
           merge_proof_branch x keep head;
           VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record (); if w = VtNow then finish ()
+          Backtrack.record (); if w == VtNow then finish ()
           
       (* Side effect on all branches *)
       | VtSideff l, w ->
@@ -1086,7 +1085,7 @@ let process_transaction verbosely (loc, expr) =
           VCS.commit id (Cmd (x,l));
           VCS.propagate_sideff (Some x);
           VCS.checkout_shallowest_proof_branch ();
-          Backtrack.record (); if w = VtNow then finish ()
+          Backtrack.record (); if w == VtNow then finish ()
 
       (* Unknown: we execute it, check for open goals and propagate sideeff *)
       | VtUnknown, VtNow ->
@@ -1117,8 +1116,8 @@ let process_transaction verbosely (loc, expr) =
     (* Proof General *)
     begin match v with 
       | VernacStm (PGLast _) ->
-        if head <> VCS.Branch.master then
-          interp dummy_state_id
+        if not (VCS.Branch.equal head VCS.Branch.master) then
+          interp Stateid.dummy
             (true,Loc.ghost,VernacShow (ShowGoal OpenSubgoals))
       | _ -> ()
     end;
@@ -1126,14 +1125,14 @@ let process_transaction verbosely (loc, expr) =
     VCS.print ()
   with e ->
     let e = Errors.push e in
-    match Stateid.get_state_id e with
+    match Stateid.get e with
     | None ->
         VCS.restore vcs;
         VCS.print ();
         anomaly (str ("execute: "^ 
           string_of_ppcmds (Errors.print_no_report e) ^ "}}}"))
     | Some (_, id) ->
-        prerr_endline ("Failed at state " ^ Stateid.string_of_state_id id);
+        prerr_endline ("Failed at state " ^ Stateid.to_string id);
         VCS.restore vcs;
         VCS.print ();
         raise e
@@ -1148,7 +1147,7 @@ let current_proof_depth () =
   | { VCS.kind = `Master } -> 0
   | { VCS.pos = cur; VCS.kind = `Proof (_,n); VCS.root = root } ->
       let rec distance cur =
-        if cur = root then 0
+        if Stateid.equal cur root then 0
         else 1 + distance (VCS.visit cur).next in
       distance cur
 
@@ -1169,7 +1168,7 @@ let get_current_proof_name () =
 
 let get_script prf =
   let rec find acc id =
-    if id = initial_state_id || id = dummy_state_id then acc else
+    if Stateid.equal id Stateid.initial || Stateid.equal id Stateid.dummy then acc else
     let view = VCS.visit id in
     match view.step with
     | `Fork (_,_,ns) when List.mem prf ns -> acc
diff --git a/toplevel/stm.mli b/toplevel/stm.mli
index c14aaf140..ca8c86d58 100644
--- a/toplevel/stm.mli
+++ b/toplevel/stm.mli
@@ -14,12 +14,12 @@ val process_transaction : bool -> Vernacexpr.located_vernac_expr -> unit
 val finish : unit -> unit
 
 (* Evaluates a particular state id (does not move the current tip) *)
-val observe : Stateid.state_id -> unit
+val observe : Stateid.t -> unit
 
 (* Joins the entire document.  Implies finish, but also checks proofs *)
 val join : unit -> unit
 
-val get_current_state : unit -> Stateid.state_id
+val get_current_state : unit -> Stateid.t
 val current_proof_depth : unit -> int
 val get_all_proof_names : unit -> Names.identifier list
 val get_current_proof_name : unit -> Names.identifier option
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index eb9f4a03d..da3049141 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -213,7 +213,7 @@ let make_prompt () =
    "n |lem1|lem2|lem3| p < "
 *)
 let make_emacs_prompt() =
-  let statnum = Stateid.string_of_state_id (Stm.get_current_state ()) in
+  let statnum = Stateid.to_string (Stm.get_current_state ()) in
   let dpth = Stm.current_proof_depth() in
   let pending = Stm.get_all_proof_names() in
   let pendingprompt =
@@ -319,9 +319,9 @@ let do_vernac () =
         Format.set_formatter_out_channel stdout;
         ppnl (print_toplevel_error any);
         pp_flush ();
-        match Stateid.get_state_id any with
+        match Stateid.get any with
         | Some (valid_id,_) ->
-            let valid = Stateid.int_of_state_id valid_id in
+            let valid = Stateid.to_int valid_id in
             Vernac.eval_expr (Loc.ghost,
               (Vernacexpr.VernacStm (Vernacexpr.Command
                 (Vernacexpr.VernacBackTo valid))))
@@ -336,7 +336,7 @@ let do_vernac () =
 let feed_emacs = function
   | { Interface.id = Interface.State id;
       Interface.content = Interface.GlobRef (_,a,_,c,_) }  -> 
-    prerr_endline ("<info>" ^"<id>"^Stateid.string_of_state_id id ^"</id>"
+    prerr_endline ("<info>" ^"<id>"^Stateid.to_string id ^"</id>"
 		   ^a^" "^c^ "</info>")
   | _  -> ()
 
diff --git a/toplevel/vernac_classifier.ml b/toplevel/vernac_classifier.ml
index 9a91786ba..ad199b0c7 100644
--- a/toplevel/vernac_classifier.ml
+++ b/toplevel/vernac_classifier.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Stateid
 open Vernacexpr
 open Errors
 open Pp
diff --git a/toplevel/vernac_classifier.mli b/toplevel/vernac_classifier.mli
index d6bc8b886..bc0c0c2b3 100644
--- a/toplevel/vernac_classifier.mli
+++ b/toplevel/vernac_classifier.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Stateid
 open Vernacexpr
 open Genarg