diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-15 13:55:45 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-15 13:55:45 +0100 |
| commit | 09a269111a4b6736118aa82667bef3abc28bd281 (patch) | |
| tree | cdb5c92c4a5ae02103b2e8e93c41246a6842a0f9 /vernac/declareDef.ml | |
| parent | a2b02cb9142984b912bf01cea09449d767326f19 (diff) | |
Fix gitlab for 4.06
Diffstat (limited to 'vernac/declareDef.ml')
0 files changed, 0 insertions, 0 deletions