aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-19 03:40:45 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-19 17:38:19 +0100
commitdc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 (patch)
tree228d0aeba91a663b947625fd58cebe5bf4537f08 /tools
parentd7a5f439de0208c4a543a81158107b8ccecb6ced (diff)
[plugins] Prepare plugin API for functional handling of state.
To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions