aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial
diff options
context:
space:
mode:
authorPierre Roux2019-03-24 22:53:38 +0100
committerPierre Roux2019-03-31 22:31:45 +0200
commit6a10b18d428178a9accd70a9717e153bb180868f (patch)
tree06972a6bfb3b4a404ea8c60f3a3f852931ad5a15 /doc/plugin_tutorial
parent93524ed2dfb3bbcc2006286954001039c95732cd (diff)
[coq] Adapt to coq/coq#9815
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions