aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-05-23 16:57:31 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2016-06-06 14:04:33 -0400
commit821937aee71bf9439158e27e06f7b4f74289b209 (patch)
tree7e06be2dbbfd3c7168a6056b4a198bad44bab1f3 /stm/stm.mli
parent8baf120d5cf5045d188f7d926162643a6e7ebcd0 (diff)
STM: proof block detection made optional + simple test
Diffstat (limited to 'stm/stm.mli')
-rw-r--r--stm/stm.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.mli b/stm/stm.mli
index 20dd40bcd..37ec1f0a1 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -130,7 +130,7 @@ module QueryTask : AsyncTaskQueue.Task
Declaration of block [-------------------------------------------]
start = 5 the first state_id that could fail in the block
- stop = 6 the node that may absorb the error
+ stop = 7 the node that may absorb the error
dynamic_switch = 4 dynamic check on this node
carry_on_data = () no need to carry extra data from static to dynamic
checks