diff options
| author | Hugo Herbelin | 2020-08-25 17:55:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-08-28 15:34:00 +0200 |
| commit | 4b9a823c03b61034e0fde76716a8623ff68977b0 (patch) | |
| tree | 8fc4f176dafa5d1332a68a57b39532c66485f8ba /dev/include | |
| parent | 9cb28c30955db553f5e2b7abe7633dec97fa9dae (diff) | |
Where there are several lists of implicit arguments, don't pretend names matter.
That is, in "About", use _ for the variables of the extra lists.
See discussion at https://github.com/coq/coq/pull/12875#issuecomment-679190489.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions