Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | | | | * | | | | | | Tweak printing boxes for unicode binders | 2018-06-10 | ||
| |_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | ||||
| | | | | | * | | | | | | | [VM] Remove projection names from structured constants. | 2018-06-10 | ||
| |_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | ||||
| | | | | * | | | | | | | Fixing #7700 (section variables bound to abbreviations were not found). | 2018-06-10 | ||
| |_|_|_|/ / / / / / / |/| | | | | | | | | | | ||||
| | * | | | | | | | | | [lib] Fix wrong deprecation comment. | 2018-06-10 | ||
| |/ / / / / / / / / |/| | | | | | | | | | ||||
* | | | | | | | | | | Merge PR #7691: Fixing spelling of statment/statement in two API types | 2018-06-09 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #7515: gitlab: build sphinx doc in separate job | 2018-06-09 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7642: Gitlab: retry failed jobs once | 2018-06-09 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | gitlab: build sphinx doc in separate job | 2018-06-08 | ||
* | | | | | | | | | | | | | Merge PR #7739: add test for #7595 | 2018-06-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7747: dev/doc/univpoly.{txt => md}, split off primitive projection ... | 2018-06-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | | | | | | Add a bit of doc to EConstr.decompose_lam* | 2018-06-08 | ||
| |_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | dev/doc/univpoly.{txt => md}, split off primitive projection info | 2018-06-08 | ||
| | | * | | | | | | | | | | | Gitlab: retry failed "build" jobs once | 2018-06-08 | ||
* | | | | | | | | | | | | | | Merge PR #7417: Micromega clean-up | 2018-06-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | Merge PR #7687: [ci] [docker] Pin specific versions of OPAM CI dependencies. | 2018-06-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | | | | | Micromega clean-up | 2018-06-07 | ||
| | | * | | | | | | | | | | | | add test for #7595 | 2018-06-07 | ||
| |_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | Merge PR #7735: Remove cross-crypto from Travis. It is still tested in GitLab... | 2018-06-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| * | | | | | | | | | | | | | | Remove cross-crypto from Travis. It is still tested in GitLab CI. | 2018-06-07 | ||
| | | | | | | | | | | | | * | | Fix the checker by merely adapting the data structure. | 2018-06-07 | ||
| | | | | | | | | | | | | * | | Fix #7615: Functor inlining drops universe substitution. | 2018-06-07 | ||
| |_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is provided | 2018-06-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | Merge PR #7706: Fix wrong deprecation msg | 2018-06-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6874: [econstr] Some minor tweaks | 2018-06-07 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7721: Add a note about [ci skip] in CI README. | 2018-06-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | | | | | | | | [ci] [docker] Pin specific versions of OPAM CI dependencies. | 2018-06-06 | ||
| |_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | | Add a note about [ci skip] in CI README. | 2018-06-06 | ||
|/ / / / / / / / / / / / / / / | ||||
* | | | | | | | | | | | | | | | Merge PR #7717: [ci] Temporal fix for CompCert | 2018-06-06 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | ||||
| * | | | | | | | | | | | | | | [ci] Temporal fix for CompCert | 2018-06-06 | ||
* | | | | | | | | | | | | | | | Merge PR #7679: Clean native compilation of primitive projections | 2018-06-05 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7004: Make `simple apply` obey `Opaque` directive. | 2018-06-05 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7077: Preserving canonical structure of return predicate in vm_comp... | 2018-06-05 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7663: test suite: make target to regenerate failing output tests | 2018-06-05 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | * | | | | | | | Improve links to SSR tactics, and some other improvements. | 2018-06-05 | ||
* | | | | | | | | | | | | | | | | | | | Merge PR #7464: Make whitespace linter not check for trailing space. | 2018-06-05 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | | | * | Define rec_declaration in terms of prec_declaration. | 2018-06-05 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | | | | | | Update evarutil.mli | 2018-06-05 | ||
| | | | | | | | * | | | | | | | | | | | Fix wrong deprecation msg | 2018-06-05 | ||
| | | | | | | | | | | | | * | | | | | | Workaround a weird error of .. coqtop:: | 2018-06-05 | ||
| | | | | | | | | | | | | * | | | | | | Remove many abusive .. coqtop in SSR chapter. | 2018-06-05 | ||
| | | | | | | | | | | | | * | | | | | | A few additional small fixes. | 2018-06-05 | ||
| | | | | | | | | | | | | * | | | | | | [sphinx] Fix missing indices warnings. | 2018-06-05 | ||
| | | | | | | | | | | | | * | | | | | | [ssr] index entry for "without loss", "suffices" and "generally have" | 2018-06-05 | ||
| | | | | | | | | | | | | * | | | | | | [ssr] some fixes to the documentation markup | 2018-06-05 | ||
| | | | | | | | | | | | | * | | | | | | [sphinx] Start fixing SSR chapter. | 2018-06-05 | ||
| |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / |/| | | | | | | | | | | | | | | | | | ||||
| | | | | * | | | | | | | | | | | | | More straightforward native compilation of primitive projections. | 2018-06-05 | ||
| | | | | * | | | | | | | | | | | | | Use projection indices in native compilation rather than constant names. | 2018-06-05 | ||
| |_|_|_|/ / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8 | 2018-06-05 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #7690: Fixing typos in file Berardi.v | 2018-06-05 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | Merge PR #7646: Fix #4714: Stack overflow with native compute | 2018-06-05 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |