aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto1
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-11-17 17:11:20 +0100
committerEmilio Jesus Gallego Arias2018-11-17 17:11:20 +0100
commitdcdd460710c36522ff10f1b12bbb0b0628c5542f (patch)
treefb2ac438846b9cbff28447a2f5e6b17c6700e3d8 /doc/plugin_tutorial/tuto1
parentf26974c7844d6a58d22c3a9d52b93c5a94f19214 (diff)
[coq] Overlay to adapt to coq/coq#9003
To be merged when the Coq developers merge the PR upstream.
Diffstat (limited to 'doc/plugin_tutorial/tuto1')
0 files changed, 0 insertions, 0 deletions