diff options
| author | Emilio Jesus Gallego Arias | 2018-02-14 06:24:02 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-02-14 06:24:02 +0100 |
| commit | 2e015ec8e2958c2848c33a152dd883e048069a7d (patch) | |
| tree | b58ab42df9c5bc08606e00a51834429b1718c783 /doc/plugin_tutorial/tuto2 | |
| parent | 46dfd18cd1744adbe9fe8463423c5a4484ebeb70 (diff) | |
[coq] Adapt to coq/coq#6745
Nothing remarkable.
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions