index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
vernac
/
g_proofs.mlg
Age
Commit message (
Expand
)
Author
2020-11-12
Revert to "using" not being a keyword in -noinit mode.
Théo Zimmermann
2020-11-12
Add support for Proof using in -noinit mode.
Théo Zimmermann
2020-06-26
[declare] [api] Removal of duplicated type aliases.
Emilio Jesus Gallego Arias
2020-05-13
Merge PR #12229: Hopefully consensual cleaning of keywords
Théo Zimmermann
2020-05-07
[declare] Merge DeclareDef into Declare
Emilio Jesus Gallego Arias
2020-05-06
Documenting plugin/tactic/stdlib keywords in corresponding chapters.
Hugo Herbelin
2020-04-21
[hints] Move and split Hint Declaration AST to vernac
Emilio Jesus Gallego Arias
2020-04-15
[proof] Merge `Proof_global` into `Declare`
Emilio Jesus Gallego Arias
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-07-01
[api] Refactor most of `Decl_kinds`
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-05-31
Remove Show Script (deprecated in 8.10)
Gaëtan Gilbert
2018-09-23
[api] Deprecate constructors of deprecated datatypes.
Emilio Jesus Gallego Arias
2018-07-07
Introduce a Pcoq.Entry module for functions that ought to be exported.
Pierre-Marie Pédrot
2018-07-02
hints: add Hint Variables/Constants Opaque/Transparent commands
Matthieu Sozeau
2018-06-29
Port g_proofs to the homebrew GEXTEND parser.
Pierre-Marie Pédrot
