index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
egramcoq.ml
Age
Commit message (
Expand
)
Author
2019-05-23
do not parse `|` as infix in patterns; parse `|}` as `|` `}`
Georges Gonthier
2019-04-02
Add parsing of decimal constants (e.g., 1.02e+01)
Pierre Roux
2019-04-02
Rename raw_natural_number to raw_numeral
Pierre Roux
2019-04-01
Replace type sign = bool with SPlus | SMinus
Pierre Roux
2019-03-31
Multiple payload types in tokens
Pierre Roux
2019-03-31
[parsing] Split Tok.t into Tok.t and Tok.pattern
Enrico Tassi
2019-01-22
Fixing #9329 (registering empty levels in the order they are recomputed).
Hugo Herbelin
2018-11-27
[gramlib] Minor cleanups:
Emilio Jesus Gallego Arias
2018-07-29
Store marshallable data in the custom entry summary.
Pierre-Marie Pédrot
2018-07-29
Supporting locality flag for custom entries + compatibility with modules.
Hugo Herbelin
2018-07-29
Adding support for custom entries in notations.
Hugo Herbelin
2018-07-07
Introduce a Pcoq.Entry module for functions that ought to be exported.
Pierre-Marie Pédrot
2018-06-29
Use a homebrew parser to replace the GEXTEND extension points of Camlp5.
Pierre-Marie Pédrot
2018-06-18
Remove reference name type.
Maxime Dénès
2018-06-12
[api] Misctypes removal: miscellaneous aliases.
Emilio Jesus Gallego Arias
2018-05-31
[notations] Split interpretation and parsing of notations
Emilio Jesus Gallego Arias
2018-05-27
[api] [parsing] Move Egram* to `vernac/`
Emilio Jesus Gallego Arias
