aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mllib
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-11-26 18:42:40 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-11-27 16:06:54 +0100
commit61209f27eb26dcb04a7d5428b9f2ab7f65f73ac8 (patch)
tree42637501f42a47cb9978663f37317b3e0a0d7b75 /stm/stm.mllib
parent10af47a5790987ee5211bac88c3a16396f30bcb0 (diff)
STM: put hooks in key events to let plugins customize the feedback
The default hook value is the one used by CoqIDE
Diffstat (limited to 'stm/stm.mllib')
0 files changed, 0 insertions, 0 deletions