aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fixes #7779 (destruct's "in" clause was forgetting the possibility of "eqn").Gravatar Hugo Herbelin2018-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
|\ \ \ \ \
* \ \ \ \ \ 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
| |/ / / / / / |/| | | | | |
| | | | | | * [VM] Remove projection names from structured constants.Gravatar Maxime Dénès2018-06-10
| |_|_|_|_|/ |/| | | | |
| | | | | * Fixing #7700 (section variables bound to abbreviations were not found).Gravatar Hugo Herbelin2018-06-10
| |_|_|_|/ |/| | | |
| | * | | [lib] Fix wrong deprecation comment.Gravatar Emilio Jesus Gallego Arias2018-06-10
| |/ / / |/| | |
* | | | Merge PR #7691: Fixing spelling of statment/statement in two API typesGravatar Pierre-Marie Pédrot2018-06-09
|\ \ \ \
* \ \ \ \ Merge PR #7515: gitlab: build sphinx doc in separate jobGravatar Emilio Jesus Gallego Arias2018-06-09
|\ \ \ \ \
* \ \ \ \ \ Merge PR #7642: Gitlab: retry failed jobs onceGravatar Emilio Jesus Gallego Arias2018-06-09
|\ \ \ \ \ \
| | * | | | | gitlab: build sphinx doc in separate jobGravatar Gaëtan Gilbert2018-06-08
* | | | | | | Merge PR #7739: add test for #7595Gravatar Gaëtan Gilbert2018-06-08
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #7747: dev/doc/univpoly.{txt => md}, split off primitive projection ...Gravatar Théo Zimmermann2018-06-08
|\ \ \ \ \ \ \ \
| | | | | | | * | Add a bit of doc to EConstr.decompose_lam*Gravatar Gaëtan Gilbert2018-06-08
| |_|_|_|_|_|/ / |/| | | | | | |
| * | | | | | | dev/doc/univpoly.{txt => md}, split off primitive projection infoGravatar Gaëtan Gilbert2018-06-08
| | | * | | | | Gitlab: retry failed "build" jobs onceGravatar Gaëtan Gilbert2018-06-08
* | | | | | | | Merge PR #7417: Micromega clean-upGravatar Théo Zimmermann2018-06-08
|\ \ \ \ \ \ \ \ | |/ / / / / / / |/| | | | | | |
* | | | | | | | Merge PR #7687: [ci] [docker] Pin specific versions of OPAM CI dependencies.Gravatar Gaëtan Gilbert2018-06-08
|\ \ \ \ \ \ \ \
| | * | | | | | | Micromega clean-upGravatar Maxime Dénès2018-06-07
| | | * | | | | | add test for #7595Gravatar Ralf Jung2018-06-07
| |_|/ / / / / / |/| | | | | | |
* | | | | | | | Merge PR #7735: Remove cross-crypto from Travis. It is still tested in GitLab...Gravatar Emilio Jesus Gallego Arias2018-06-07
|\ \ \ \ \ \ \ \
| * | | | | | | | Remove cross-crypto from Travis. It is still tested in GitLab CI.Gravatar Théo Zimmermann2018-06-07
* | | | | | | | | Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is providedGravatar Matthieu Sozeau2018-06-07
|\ \ \ \ \ \ \ \ \ | |/ / / / / / / / |/| | | | | | | |
* | | | | | | | | Merge PR #7706: Fix wrong deprecation msgGravatar Pierre-Marie Pédrot2018-06-07
|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ Merge PR #6874: [econstr] Some minor tweaksGravatar Pierre-Marie Pédrot2018-06-07
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7721: Add a note about [ci skip] in CI README.Gravatar Emilio Jesus Gallego Arias2018-06-06
|\ \ \ \ \ \ \ \ \ \ \
| | | | | * | | | | | | [ci] [docker] Pin specific versions of OPAM CI dependencies.Gravatar Emilio Jesus Gallego Arias2018-06-06
| |_|_|_|/ / / / / / / |/| | | | | | | | | |
| * | | | | | | | | | Add a note about [ci skip] in CI README.Gravatar Théo Zimmermann2018-06-06
|/ / / / / / / / / /
* | | | | | | | | | Merge PR #7717: [ci] Temporal fix for CompCertGravatar Gaëtan Gilbert2018-06-06
|\ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / |/| | | | | | | | |
| * | | | | | | | | [ci] Temporal fix for CompCertGravatar Emilio Jesus Gallego Arias2018-06-06
* | | | | | | | | | Merge PR #7679: Clean native compilation of primitive projectionsGravatar Maxime Dénès2018-06-05
|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ Merge PR #7004: Make `simple apply` obey `Opaque` directive.Gravatar Pierre-Marie Pédrot2018-06-05
|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ Merge PR #7077: Preserving canonical structure of return predicate in vm_comp...Gravatar Maxime Dénès2018-06-05
|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ Merge PR #7663: test suite: make target to regenerate failing output testsGravatar Enrico Tassi2018-06-05
|\ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | | | | | * | Improve links to SSR tactics, and some other improvements.Gravatar Théo Zimmermann2018-06-05
* | | | | | | | | | | | | | Merge PR #7464: Make whitespace linter not check for trailing space.Gravatar Maxime Dénès2018-06-05
|\ \ \ \ \ \ \ \ \ \ \ \ \ \
| | | | | | | | * | | | | | | Update evarutil.mliGravatar Matthieu Sozeau2018-06-05
| | | | | | | | * | | | | | | Fix wrong deprecation msgGravatar Matthieu Sozeau2018-06-05
| | | | | | | | | | | | | * | Workaround a weird error of .. coqtop::Gravatar Théo Zimmermann2018-06-05
| | | | | | | | | | | | | * | Remove many abusive .. coqtop in SSR chapter.Gravatar Théo Zimmermann2018-06-05
| | | | | | | | | | | | | * | A few additional small fixes.Gravatar Théo Zimmermann2018-06-05
| | | | | | | | | | | | | * | [sphinx] Fix missing indices warnings.Gravatar Théo Zimmermann2018-06-05
| | | | | | | | | | | | | * | [ssr] index entry for "without loss", "suffices" and "generally have"Gravatar Enrico Tassi2018-06-05
| | | | | | | | | | | | | * | [ssr] some fixes to the documentation markupGravatar Enrico Tassi2018-06-05
| | | | | | | | | | | | | * | [sphinx] Start fixing SSR chapter.Gravatar Théo Zimmermann2018-06-05
| |_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | |