index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
Commit message (
Expand
)
Author
Age
...
*
|
|
|
Merge PR #6183: [plugins] Prepare plugin API for functional handling of state.
Maxime Dénès
2017-11-20
|
\
\
\
\
*
\
\
\
\
Merge PR #6163: [dev] Remove deprecation warning from `base_include`
Maxime Dénès
2017-11-20
|
\
\
\
\
\
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
*
|
Add Equations to CI
Matthieu Sozeau
2017-11-20
|
|
_
|
/
/
|
/
|
|
|
|
|
|
*
[parser] Remove unnecessary statically initialized hook.
Emilio Jesus Gallego Arias
2017-11-19
|
|
_
|
/
|
/
|
|
|
|
*
[plugins] Prepare plugin API for functional handling of state.
Emilio Jesus Gallego Arias
2017-11-19
|
|
/
|
/
|
*
|
Merge PR #6148: [api] Another large deprecation, `Nameops` and friends.
Maxime Dénès
2017-11-16
|
\
\
|
|
*
[dev] Remove deprecation warning from `base_include`
Emilio Jesus Gallego Arias
2017-11-15
|
|
/
|
/
|
|
*
[api] Another large deprecation, `Nameops`
Emilio Jesus Gallego Arias
2017-11-13
*
|
Change OCAMLRUNPARAM warning to mention OCaml 4.06
Paul Steckler
2017-11-13
|
/
*
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Maxime Dénès
2017-11-13
|
\
*
\
Merge PR #6126: Fix ci-bignums.sh "missing ]" error.
Maxime Dénès
2017-11-13
|
\
\
*
\
\
Merge PR #6124: Adding a debugging printer for ident maps whose codomain type...
Maxime Dénès
2017-11-13
|
\
\
\
*
\
\
\
Merge PR #6071: [ci] Add Ltac2
Maxime Dénès
2017-11-13
|
\
\
\
\
*
\
\
\
\
Merge PR #6065: [api] Deprecate all legacy uses of Names in core.
Maxime Dénès
2017-11-13
|
\
\
\
\
\
|
|
|
|
*
|
Fix ci-bignums.sh "missing ]" error.
Gaëtan Gilbert
2017-11-09
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
*
|
Adding a debugging printer for ident maps whose codomain type is unknown.
Hugo Herbelin
2017-11-08
*
|
|
|
|
Merge PR #6100: [api] Remove 8.7 ML-deprecated functions.
Maxime Dénès
2017-11-08
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6086: [ci] Switch VST back to upstream.
Maxime Dénès
2017-11-08
|
\
\
\
\
\
\
|
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
*
|
|
|
[api] Remove 8.7 ML-deprecated functions.
Emilio Jesus Gallego Arias
2017-11-07
|
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
*
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
|
|
|
|
/
|
|
|
/
|
|
|
*
|
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
|
|
/
/
|
/
|
|
*
|
|
Merge PR #6049: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" ...
Maxime Dénès
2017-11-06
|
\
\
\
*
\
\
\
Merge PR #1139: Add a linter.
Maxime Dénès
2017-11-06
|
\
\
\
\
|
|
|
|
*
[ci] Add Ltac2
Jason Gross
2017-11-04
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
Merge PR #6047: A generic printer for ltac values
Maxime Dénès
2017-11-03
|
\
\
\
\
*
\
\
\
\
Merge PR #6036: [toplevel] Export the last document seen after `Drop`.
Maxime Dénès
2017-11-03
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #6031: [ci] Switch back to upstream version of Math-Classes and Corn.
Maxime Dénès
2017-11-03
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #6027: Mention the migration from Bugzilla to GitHub issues in dev/d...
Maxime Dénès
2017-11-03
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #6024: Update of Coq version history
Maxime Dénès
2017-11-03
|
\
\
\
\
\
\
\
\
|
|
|
|
|
*
|
|
|
Using a specific function to register vernac printers.
Hugo Herbelin
2017-11-02
|
|
_
|
_
|
_
|
/
/
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules
Matej Košík
2017-11-01
|
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
[ci] Switch VST back to upstream.
Théo Zimmermann
2017-10-30
|
|
|
|
|
_
|
/
|
|
|
|
/
|
|
|
|
|
|
*
|
[toplevel] Export the last document seen after `Drop`.
Emilio Jesus Gallego Arias
2017-10-28
|
|
|
*
|
|
[ci] Switch back to upstream version of Math-Classes and Corn.
Théo Zimmermann
2017-10-27
|
|
|
|
/
/
|
|
*
/
/
Mention the migration from Bugzilla to GitHub issues in dev/doc/changes.
Théo Zimmermann
2017-10-27
|
|
|
/
/
*
|
|
|
Merge PR #6015: [general] Remove Econstr dependency from `intf`
Maxime Dénès
2017-10-27
|
\
\
\
\
*
\
\
\
\
Merge PR #677: Trunk+abstracting injection flags
Maxime Dénès
2017-10-27
|
\
\
\
\
\
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
*
|
|
|
Passing around the flag for injection so that tactics calling inj at
Hugo Herbelin
2017-10-26
|
|
|
*
|
Updating version history wrt 8.7.
Hugo Herbelin
2017-10-26
|
|
|
*
|
Updating version history wrt 8.6.
Hugo Herbelin
2017-10-26
|
|
|
*
|
Updating version history wrt 8.5.
Hugo Herbelin
2017-10-26
|
|
_
|
/
/
|
/
|
|
|
|
|
*
|
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-10-25
|
|
/
/
|
|
*
Linter: check that files end with newlines.
Gaëtan Gilbert
2017-10-25
|
|
*
Put newlines at the end of files.
Gaëtan Gilbert
2017-10-25
|
|
*
Add linter.
Gaëtan Gilbert
2017-10-25
*
|
|
Merge PR #6003: Point HoTT back at master, which now supports Coq master
Maxime Dénès
2017-10-25
|
\
\
\
|
*
|
|
Point HoTT back at master, which now supports Coq master
Jason Gross
2017-10-23
*
|
|
|
Switch testing branch back to CompCert upstream.
Théo Zimmermann
2017-10-20
|
|
/
/
|
/
|
|
*
|
|
Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than just...
Maxime Dénès
2017-10-20
|
\
\
\
|
*
|
|
rename ci-iris-coq -> ci-iris-lambda-rust
Ralf Jung
2017-10-19
[prev]
[next]
Maxime Dénès
Matthieu Sozeau
Emilio Jesus Gallego Arias
Paul Steckler
Gaëtan Gilbert
Hugo Herbelin
Jason Gross
Matej Košík
Théo Zimmermann
Ralf Jung