diff options
| author | Emilio Jesus Gallego Arias | 2018-11-28 02:47:20 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-28 02:47:20 +0100 |
| commit | df40307f70d7a03b03af7ae4360a15349abc1bd0 (patch) | |
| tree | 19f86f4660aaa697199a27cecc64e85b082d2d92 /doc/plugin_tutorial/tuto0 | |
| parent | b5ebc0a2aa4e73054b6085dd82211a08636c1418 (diff) | |
[coq overlay] Adapt to coq/coq#8705
Please apply when indicated.
Diffstat (limited to 'doc/plugin_tutorial/tuto0')
0 files changed, 0 insertions, 0 deletions