X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fstate.ml;h=4b02d596c1430153e58185ca069bc9d820e639d3;hp=bb7a06393cc75e880211b9e01c0b571386ed3483;hb=4f265eb7d78b740292b5543d94f9f0fa40d206d5;hpb=974dacbf4f625bfd8ea83db69d6b346050141fea

diff --git a/src/state.ml b/src/state.ml
index bb7a063..4b02d59 100644
--- a/src/state.ml
+++ b/src/state.ml
@@ -13,28 +13,15 @@
 (*                                                                     *)
 (***********************************************************************)
 
-(*
-  Time-stamp: <Last modified on 2013-04-04 18:45:59 CEST by Kim Nguyen>
-*)
-
 open Format
+include Hcons.PosInt
 
-type t = int
-let make =
+let next =
   let id = ref ~-1 in
-    fun () -> incr id; !id
-
-let compare = (-)
-
-let equal = (==)
-
-external hash : t -> int =  "%identity"
-
-let print fmt x = fprintf fmt "q%a" Pretty.pp_subscript x
+    fun () -> incr id; make !id
 
-let dump fmt x = print fmt x
+let compare (a : t) (b : t) = (a :> int) - (b :> int)
 
-let check x =
-  if x < 0 then failwith (Printf.sprintf "State: Assertion %i < 0 failed" x)
+let print fmt (x : t) = fprintf fmt "q%a" Pretty.pp_subscript (x :> int)
 
-let dummy = max_int
+let dummy_state = make max_int