1 files changed, 27 insertions, 23 deletions
diff --git a/stm/dag.mli b/stm/dag.mli
index 6b4442df..e783cd8e 100644
--- a/stm/dag.mli
+++ b/stm/dag.mli
@@ -7,19 +7,7 @@
 (************************************************************************)
 
 module type S = sig
-
-  (* A cluster is just a set of nodes.  This set holds some data.
-     Stm uses this to group nodes contribution to the same proofs and
-     that can be evaluated asynchronously *)
-  module Cluster :
-  sig
-    type 'd t
-    val equal : 'd t -> 'd t -> bool
-    val compare : 'd t -> 'd t -> int
-    val to_string : 'd t -> string
-    val data : 'd t -> 'd
-  end
-
+  
   type node
   module NodeSet : Set.S with type elt = node
 
@@ -34,19 +22,35 @@ module type S = sig
   val del_nodes : ('e,'i,'d) t -> NodeSet.t  -> ('e,'i,'d) t
   val all_nodes : ('e,'i,'d) t -> NodeSet.t
 
-  val iter : ('e,'i,'d) t -> 
-    (node -> 'd Cluster.t option -> 'i option ->
-      (node * 'e) list -> unit) -> unit
-
-  val create_cluster : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
-  val cluster_of : ('e,'i,'d) t -> node -> 'd Cluster.t option
-  val del_cluster : ('e,'i,'d) t -> 'd Cluster.t -> ('e,'i,'d) t
-
   val get_info : ('e,'i,'d) t -> node -> 'i option
   val set_info : ('e,'i,'d) t -> node -> 'i -> ('e,'i,'d) t
   val clear_info : ('e,'i,'d) t -> node -> ('e,'i,'d) t
 
-end
+  (* A property applies to a set of nodes and holds some data.
+     Stm uses this feature to group nodes contributing to the same proofs and
+     to structure proofs in boxes limiting the scope of errors *)
+  module Property :
+  sig
+    type 'd t
+    val equal : 'd t -> 'd t -> bool
+    val compare : 'd t -> 'd t -> int
+    val to_string : 'd t -> string
+    val data : 'd t -> 'd
+    val having_it : 'd t -> NodeSet.t
+  end
+
+  val create_property : ('e,'i,'d) t -> node list -> 'd -> ('e,'i,'d) t
+  val property_of : ('e,'i,'d) t -> node -> 'd Property.t list
+  val del_property : ('e,'i,'d) t -> 'd Property.t -> ('e,'i,'d) t
+
+  val iter : ('e,'i,'d) t -> 
+    (node -> 'd Property.t list -> 'i option ->
+      (node * 'e) list -> unit) -> unit
+
+  end
 
-module Make(OT : Map.OrderedType) : S with type node = OT.t
+module Make(OT : Map.OrderedType) : S
+with type node = OT.t
+and type NodeSet.t = Set.Make(OT).t
+and type NodeSet.elt = OT.t