aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto2/src/persistent_counter.mli
diff options
context:
space:
mode:
authorJim Fehrle2020-06-06 14:18:20 -0700
committerJim Fehrle2020-06-06 14:18:20 -0700
commitc964091f01af77bb9aff14cb25bc4d8466c5239d (patch)
tree0f7359efbdf599201de43a4118240777cfbe7fb7 /doc/plugin_tutorial/tuto2/src/persistent_counter.mli
parent9c26e583668827bff5159e7671c406ace8b2f3ae (diff)
Match only a single line as the coqtop prompt
(the previous expression was including some expected output)
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src/persistent_counter.mli')
0 files changed, 0 insertions, 0 deletions