diff options
| author | Hugo Herbelin | 2020-08-27 14:48:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | d07d14dfd82cd08564ef0513c23236d73a67664f (patch) | |
| tree | f0584509b4390135114e417a37b0c60c41a289eb /dev | |
| parent | 4b9a823c03b61034e0fde76716a8623ff68977b0 (diff) | |
About: Add a mention that arguments have been renamed, if ever it is the case.
See https://github.com/coq/coq/pull/12875#issuecomment-679190489.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions