aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1
diff options
context:
space:
mode:
authorHugo Herbelin2020-02-23 17:11:01 +0100
committerHugo Herbelin2020-02-23 18:05:32 +0100
commit267f981c5c05cd795e08ea14aaeab5a49550d21b (patch)
tree994c843c222967bfd8a81e185e2d7c697d933219 /doc/plugin_tutorial/tuto1
parent61f2f55a08dcef612c538ec7e6d0864d86fe3e0a (diff)
Adding a Display Parentheses menu in CoqIDE.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions