aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* | | | | | | | | | | | | | 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
| |_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | |
| | | | | | * | | | | | | | | [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 script] Check if the CI that was run is outdated.Gravatar Théo Zimmermann2018-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
| |_|_|_|_|_|/ / / / / / / / / |/| | | | | | | | | | | | | |
| | | | | | | | | | | | | | * [doc] Disable smartquotes conversionGravatar Clément Pit-Claudel2018-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
| | | | | | | | | | | | | * | Fix the checker by merely adapting the data structure.Gravatar Pierre-Marie Pédrot2018-06-07
| | | | | | | | | | | | | * | Fix #7615: Functor inlining drops universe substitution.Gravatar Pierre-Marie Pédrot2018-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
|\ \ \ \ \ \ \ \ \ \ \ \ \ \