Change Implicit Arguments to Arguments
c.f. discussion in 78e75ff1 (comment 76147)
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)