index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
pvernac.mli
Age
Commit message (
Expand
)
Author
2020-10-27
Rename misc nonterminals
Jim Fehrle
2020-10-04
Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."
Jim Fehrle
2020-05-07
[declare] Merge DeclareDef into Declare
Emilio Jesus Gallego Arias
2020-04-21
[hints] Move and split Hint Declaration AST to vernac
Emilio Jesus Gallego Arias
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-07-23
[vernacexpr] Refactor fixpoint AST.
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-04-25
[vernac] [ast] Make location info an attribute of vernaculars.
Emilio Jesus Gallego Arias
2019-02-05
[parsing] Use AST node for main parsing entry.
Emilio Jesus Gallego Arias
2019-01-24
[STM] explicit handling of parsing states
Enrico Tassi
2018-07-07
Introduce a Pcoq.Entry module for functions that ought to be exported.
Pierre-Marie Pédrot
2018-05-30
Move interning the [hint_pattern] outside the Typeclasses hooks.
Gaëtan Gilbert
2018-05-27
[api] Make `vernac/` self-contained.
Emilio Jesus Gallego Arias