aboutsummaryrefslogtreecommitdiff
path: root/vernac/comArguments.ml
AgeCommit message (Expand)Author
2020-08-28When reporting an implicit argument error on a rename argument, use the renam...Hugo Herbelin
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-04-15Add needed commas in messageJim Fehrle
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2019-11-20make VernacArguments closer to user syntaxGaëtan Gilbert
2019-10-31Move Arguments implementation to its own file (from vernacentries)Gaëtan Gilbert