diff options
| author | Emilio Jesus Gallego Arias | 2018-12-17 19:01:04 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-09 17:46:36 +0100 |
| commit | 67cff8c545a25e7fa1a29b08d41fc64a7278508b (patch) | |
| tree | 99f3a46374bdecb25f16bd1109f6d8e690071841 /doc/plugin_tutorial/tuto3/src | |
| parent | 2216604fb42a4fe2013e25d95e0c6a5f715db287 (diff) | |
[coq] Adapt to coq/coq#9137
To be merged when the upstream PR is merged.
Not sure this is the right thing to do tho.
Diffstat (limited to 'doc/plugin_tutorial/tuto3/src')
0 files changed, 0 insertions, 0 deletions