Change Implicit Arguments to Arguments
c.f. https://github.com/coq/coq/pull/6802
c.f. discussion in 78e75ff1 (comment 76147)
0001-Change-Implicit-Arguments-to-Arguments.patch
The attached patch file changes Implicit Arguments
commands to Arguments
commands in a way that compiles with Coq 8.4 and Coq 8.7 (and should work for the whole range 8.4-8.8).
In previous discussion, 8.4 was said to have a broken Arguments
command; other than needing to explicitly give trailing arguments, I didn't observe much variation from modern behavior. If there are fundamental problems with Arguments
in 8.4, this may be a non-starter, but these changes seem to work.
(This issue is essentially a pull/merge request, since I don't know how to create a fork)