From d75da809429d5d2d40d108608db9e5acd9aec9c9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 23 May 2016 11:08:37 +0200
Subject: STM: support for nested boxes of nodes to model error boundaries

Dag extended to support arbitrary clusters, renamed to Property.
Vcs generalized to not impose the data hold by a Property.
Stm(VCS) names a property "a box" and imposes a topological invariant (no
overlap).  It defines 2 kind of boxes: ProofTasks (the old cluster
notion) and ErrorBound (meant to confine errors to sub-proofs).

In the meanwhile more equations added to Make(..) functors in order to
have just one Stateid.Set module around.
---
 lib/stateid.ml | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'lib/stateid.ml')

diff --git a/lib/stateid.ml b/lib/stateid.ml
index c17df2b32..500581a39 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -29,7 +29,13 @@ let get exn = Exninfo.get exn state_id_info
 let equal = Int.equal
 let compare = Int.compare
 
-module Set = Set.Make(struct type t = int let compare = compare end)
+module Self = struct
+ type t = int
+ let compare = compare
+ let equal = equal
+end
+
+module Set = Set.Make(Self)
 
 type ('a,'b) request = {
   exn_info : t * t;
-- 
cgit v1.2.3