diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-05-23 11:11:30 +0200 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-06 05:48:44 -0400 |
commit | 5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 (patch) | |
tree | c803222d842bd96f3a25852633288e3aab14f45f /stm/stm.mllib | |
parent | 07115d044cb97bc6c0a7323783d4d53e083d3e89 (diff) |
STM: proof block detection/error resilience API
This commit introduces the concept of proof blocks that are
resilient to errors. They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.
The detection and error recovery of ErrorBound boxes is defined outside
the STM. One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.
Diffstat (limited to 'stm/stm.mllib')
0 files changed, 0 insertions, 0 deletions