aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Add introduction and credits to the TOC.Gravatar Théo Zimmermann2018-06-17
* Move indexes on top on the TOC. Closes #7764.Gravatar Théo Zimmermann2018-06-17
* Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretypingGravatar Pierre-Marie Pédrot2018-06-17
|\
* \ Merge PR #7749: [doc] Disable smartquotes conversionGravatar Maxime Dénès2018-06-17
|\ \
* \ \ Merge PR #7752: [merge script] Check if the CI that was run is outdated.Gravatar Maxime Dénès2018-06-17
|\ \ \
* \ \ \ Merge PR #7635: Define rec_declaration in terms of prec_declaration.Gravatar Maxime Dénès2018-06-17
|\ \ \ \
* \ \ \ \ Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.Gravatar Maxime Dénès2018-06-17
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7814: doc: Add "Print Canonical Projections" command to Command indexGravatar Théo Zimmermann2018-06-16
|\ \ \ \ \ \
| * | | | | | [sphinx] Finish clean-up of the Canonical Structure subsection.Gravatar Théo Zimmermann2018-06-16
| * | | | | | doc: Add "Print Canonical Projections" command to Command indexGravatar Anton Trunov2018-06-16
|/ / / / / /
* | | | | | Merge PR #7813: Workaround for #2800: handling non-value arguments in tactics.Gravatar Pierre-Marie Pédrot2018-06-15
|\ \ \ \ \ \
| | | | | | * Do not allow spliting in res_pf, this is reserved for pretypingGravatar Matthieu Sozeau2018-06-15
| |_|_|_|_|/ |/| | | | |
| * | | | | Workaround to handle non-value arguments in tactics.Gravatar Cyprien Mangin2018-06-14
* | | | | | Merge PR #7803: [TYPO FIX] elimitate -> eliminateGravatar Hugo Herbelin2018-06-14
|\ \ \ \ \ \ | |/ / / / / |/| | | | |
* | | | | | Merge PR #7793: [ci] update docker image to include elpi 1.0.4Gravatar Emilio Jesus Gallego Arias2018-06-14
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #7809: Fix deprecation warning introduced by PR 664 mergeGravatar Pierre-Marie Pédrot2018-06-14
|\ \ \ \ \ \ \
| * | | | | | | Fix deprecation warning introduced by PR 664 mergeGravatar Matthieu Sozeau2018-06-14
* | | | | | | | Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ...Gravatar Pierre-Marie Pédrot2018-06-14
|\ \ \ \ \ \ \ \ | |/ / / / / / / |/| | | | | | |
* | | | | | | | Merge PR #664: Fixing #5500 (missing test in return clause of match leading t...Gravatar Matthieu Sozeau2018-06-14
|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder i...Gravatar Matthieu Sozeau2018-06-14
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7105: Getting rid of some false "collision between bound variable n...Gravatar Matthieu Sozeau2018-06-14
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7771: Tweak printing boxes for unicode bindersGravatar Hugo Herbelin2018-06-14
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | | * | | | | [TYPO FIX] elimitate -> eliminateGravatar Siddharth2018-06-14
| |_|_|_|_|_|/ / / / / |/| | | | | | | | | |
* | | | | | | | | | | Merge PR #7790: [ci] Require runner `docker` tag on `docker-boot` job.Gravatar Gaëtan Gilbert2018-06-14
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7785: Document how to restart failed CI jobs.Gravatar Emilio Jesus Gallego Arias2018-06-13
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7800: Markdown docs: switch from absolute to relative links.Gravatar Emilio Jesus Gallego Arias2018-06-13
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | * | | | | [ci] update docker image to include elpi 1.0.4Gravatar Enrico Tassi2018-06-13
| | * | | | | | | | | | | | Document how to restart failed CI jobs.Gravatar Théo Zimmermann2018-06-13
| |/ / / / / / / / / / / /
| * / / / / / / / / / / / Markdown docs: switch from absolute to relative links.Gravatar Théo Zimmermann2018-06-13
|/ / / / / / / / / / / /
* | | | | | | | | | | | Merge PR #7241: [coq_makefile] COQMF_WINDRIVE is empty on linux (fix #7233)Gravatar Théo Zimmermann2018-06-13
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7789: Fixes #7779: destruct's "in" clause was forgetting the possib...Gravatar Pierre-Marie Pédrot2018-06-13
|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7677: [api] Remove MisctypesGravatar Pierre-Marie Pédrot2018-06-13
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7782: [VM] Rename reloc -> cenvGravatar Pierre-Marie Pédrot2018-06-13
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|/ / / / / |/| | | | | | | | | | | | | |
| | | | | * | | | | | | | | | [ci] Require runner `docker` tag on `docker-boot` job.Gravatar Emilio Jesus Gallego Arias2018-06-12
| |_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | |
| | | * | | | | | | | | | | Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Gravatar Hugo Herbelin2018-06-12
| | * | | | | | | | | | | | [api] Add compatiblity Misctypes module.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | * | | | | | | | | | | | [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | * | | | | | | | | | | | [api] Misctypes removal: tactic flags.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | * | | | | | | | | | | | [api] Misctypes removal: move Tactypes to proofsGravatar Emilio Jesus Gallego Arias2018-06-12
| | * | | | | | | | | | | | [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
| | * | | | | | | | | | | | [api] Misctypes removal: remove dummy alias.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | * | | | | | | | | | | | [api] Misctypes removal: miscellaneous aliases.Gravatar Emilio Jesus Gallego Arias2018-06-12
| | * | | | | | | | | | | | [api] Misctypes removal: module_kind to DeclaremodsGravatar Emilio Jesus Gallego Arias2018-06-12
| | * | | | | | | | | | | | [api] Misctypes removal: multi to tactics/rewriteGravatar Emilio Jesus Gallego Arias2018-06-12
| |/ / / / / / / / / / / / |/| | | | | | | | | | | |
* | | | | | | | | | | | | Merge PR #7008: Bump version number to 8.9+alpha1Gravatar Guillaume Melquiond2018-06-12
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |_|/ / / / / / / / / / / |/| | | | | | | | | | | |
| | | | | | * | | | | | | Fixes #7780 (missing lift in expanding alias under a binder in unification).Gravatar Hugo Herbelin2018-06-12
| |_|_|_|_|/ / / / / / / |/| | | | | | | | | | |
| | * | | | | | | | | | [VM] Rename reloc -> cenvGravatar Maxime Dénès2018-06-12
| |/ / / / / / / / / / |/| | | | | | | | | |
* | | | | | | | | | | Merge PR #6827: [VM] Remove projection names from structured constants.Gravatar Pierre-Marie Pédrot2018-06-11
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7761: Fixing #7700: section variables bound to abbreviations were n...Gravatar Emilio Jesus Gallego Arias2018-06-11
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7406: Fix #7214: install knows which ml files do not get compiled t...Gravatar Pierre-Marie Pédrot2018-06-11
|\ \ \ \ \ \ \ \ \ \ \ \ \