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