index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
plugins
/
derive
/
g_derive.mlg
Age
Commit message (
Expand
)
Author
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-11
STM: encode in static types that vernac_when is only used when VtSideff
Gaëtan Gilbert
2019-06-09
[proof] Move proofs that have an associated constant to `Lemmas`
Emilio Jesus Gallego Arias
2019-06-04
Alternate syntax for ![]: VERNAC EXTEND Foo STATE proof
Gaëtan Gilbert
2019-06-04
coqpp: add new ![] specifiers for structured proof interaction
Gaëtan Gilbert
2019-06-04
Proof_global: pass only 1 pstate when we don't want the proof stack
Gaëtan Gilbert
2019-03-27
[plugins] [derive] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2019-01-24
[STM] explicit handling of parsing states
Enrico Tassi
2018-11-17
[vernacextend] Consolidate extension points API
Emilio Jesus Gallego Arias
2018-10-02
Make the coqpp VERNAC EXTEND behave as the non-FUNCTIONAL camlp5 one.
Pierre-Marie Pédrot
2018-10-02
Port g_derive to coqpp.
Pierre-Marie Pédrot
