diff options
| author | Maxime Dénès | 2018-06-18 14:21:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-06-18 17:14:24 +0200 |
| commit | eba6d1ffe7a3aa775e6a4984914461364149573f (patch) | |
| tree | 43fe81addd3a3d55968b9e15a29a0332155491ad /doc/plugin_tutorial | |
| parent | 15010cea58df81a3ccfdd5a4b2a01375e34853f3 (diff) | |
Adapt to Coq's PR #7797 (removal of reference).
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions