aboutsummaryrefslogtreecommitdiff
path: root/vernac/comArguments.ml
AgeCommit message (Collapse)Author
2020-11-27Fix #13283: improved error on `clear implicit` flagFabian Kunze
2020-08-28When reporting an implicit argument error on a rename argument, use the ↵Hugo Herbelin
renaming. Example: > Arguments id [B] {b} : rename. > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Error: Argument B is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
Try just going with the user-given names, and not worrying about what happens with repeated names or anonymous implicits. (Support for anonymous implicits is due to herbelin in #11098.) This PR should not change behaviour in the absence of repeated names. Since repeated names are already a poorly handled corner case, I would recommend changing binder names to avoid overlap in the case of a change in behavior. Since anonymous implicits and implicits with repeated names can already happen, I think this is unlikely to cause too many new problems, though it might exacerbate existing ones. However, I already had to fix one newly possible anomaly, so I can't be too confident. The most common change in external developments was that an argument no longer gets `0` appended to it, causing the `Arguments` command to complain about renaming. To fix this and keep the old name, one can simply use the `rename` flag as suggested, or switch to the new, un-suffixed name. Closes #6785 Closes #12001 Another step towards checking the standard library with `-mangle-names`.
2020-04-15Add needed commas in messageJim Fehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2019-11-20make VernacArguments closer to user syntaxGaëtan Gilbert
ie keep the fake arguments "/" and "&" instead of getting their index at parsing time.
2019-10-31Move Arguments implementation to its own file (from vernacentries)Gaëtan Gilbert