aboutsummaryrefslogtreecommitdiff
path: root/vernac/comArguments.mli
AgeCommit message (Collapse)Author
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