diff options
| author | Hugo Herbelin | 2018-05-25 16:04:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-05-25 17:21:38 +0200 |
| commit | e15c228709351f5001f6a10765a816cebcf900cc (patch) | |
| tree | a8719ab13b47ebc8e7184cebe3640d84f04d7b9d /doc/plugin_tutorial/tuto2 | |
| parent | 5eb92624f33afb4d2a390f7c7b80552e3e04bc81 (diff) | |
Renaming global_reference according to Coq PR #6156.
Diffstat (limited to 'doc/plugin_tutorial/tuto2')
0 files changed, 0 insertions, 0 deletions