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 #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
|
*
|
|
CI: build lambdaRust (which depends on Iris) rather than just Iris
Ralf Jung
2017-10-19
|
|
/
/
*
/
/
Bugzilla autolink: avoid linking inside links (fix #5974).
Gaëtan Gilbert
2017-10-18
|
/
/
*
|
Merge PR #540: [configure] Support for flambda flags.
Maxime Dénès
2017-10-10
|
\
\
*
\
\
Merge PR #1067: Iris CI: use opam to install dependencies
Maxime Dénès
2017-10-10
|
\
\
\
|
|
*
|
[configure] Support for flambda flags.
Emilio Jesus Gallego Arias
2017-10-10
|
|
/
/
|
/
|
|
*
|
|
Merge PR #1115: Autolink to Github PRs from Bugzilla
Maxime Dénès
2017-10-09
|
\
\
\
*
\
\
\
Merge PR #1117: [ci] Remove temporary bignums overlay.
Maxime Dénès
2017-10-09
|
\
\
\
\
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
Extract changes to the XML protocol from its doc
Théo Zimmermann
2017-10-06
*
|
|
|
Make the XML protocol doc more version-independent
Théo Zimmermann
2017-10-06
[next]
Maxime Dénès
Gaëtan Gilbert
Hugo Herbelin
Emilio Jesus Gallego Arias
Jason Gross
Matej Košík
Théo Zimmermann
Ralf Jung