index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
toplevel
/
g_toplevel.mlg
Age
Commit message (
Expand
)
Author
2020-10-09
Add an XML message for "Show Proof Diffs"
Jim Fehrle
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-01
[parser] lk_int -> lk_nat
Maxime Dénès
2020-03-01
Refactor lookaheads using DSL
Maxime Dénès
2019-10-29
Show diffs in "Show Proof."
Jim Fehrle
2019-07-29
Tentatively providing a localization function to ad-hoc camlp5 parsers.
Pierre-Marie Pédrot
2019-07-25
Remove deprecated `Backtrack` command
Maxime Dénès
2019-06-25
Re-add the "Show Goal" command for Prooftree in PG.
Jim Fehrle
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-06-29
Port g_toplevel to the homebrew GEXTEND parser.
Pierre-Marie Pédrot
