aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Remove Elpi from Travis.Gravatar Théo Zimmermann2018-06-16
* 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
|\
| * 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
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #7748: Add a bit of doc to EConstr.decompose_lam*Gravatar Pierre-Marie Pédrot2018-06-11
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7757: [lib] Fix wrong deprecation comment.Gravatar Pierre-Marie Pédrot2018-06-11
|\ \ \ \ \ \ \ \ \ \ \
| | | | | | * | | | | | Bump version number to 8.9+alpha1Gravatar Maxime Dénès2018-06-11
| |_|_|_|_|/ / / / / / |/| | | | | | | | | |
* | | | | | | | | | | Merge PR #7736: [ci] Fix GeoCoq after https://github.com/GeoCoq/GeoCoq/issues/12Gravatar Gaëtan Gilbert2018-06-11
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7284: [sphinx] Start fixing SSR chapter.Gravatar Maxime Dénès2018-06-11
|\ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | [ci] GeoCoq now depends on math-comp's ssralg.Gravatar Emilio Jesus Gallego Arias2018-06-11
| |/ / / / / / / / / / / |/| | | | | | | | | | |
| | | | | | | | * | | | Tweak printing boxes for unicode bindersGravatar Ralf Jung2018-06-10
| |_|_|_|_|_|_|/ / / / |/| | | | | | | | | |