| Age | Commit message (Expand) | Author |
|---|
| 2020-11-15 | Merge PR #13339: In -noinit mode, add support for Proof using, using is not a... | Pierre-Marie Pédrot |
| 2020-11-15 | Merge PR #13350: Fix incorrect "avoid" set in globenv extra data | Pierre-Marie Pédrot |
| 2020-11-15 | Merge PR #13356: Make the universe of primitive arrays irrelevant | Pierre-Marie Pédrot |
| 2020-11-14 | Merge PR #13369: Move destructuring let syntax closer to its documentation. | coqbot-app[bot] |
| 2020-11-14 | Move destructuring let syntax closer to its documentation. | Théo Zimmermann |
| 2020-11-13 | Merge PR #13358: Merge the Linked / LinkedInteractive native link information... | coqbot-app[bot] |
| 2020-11-13 | Fix incorrect "avoid" set in globenv extra data | Gaëtan Gilbert |
| 2020-11-13 | Make the universe of primitive arrays irrelevant | Gaëtan Gilbert |
| 2020-11-13 | Remove unused CClosure.FNativeEntries.farray | Gaëtan Gilbert |
| 2020-11-13 | Merge PR #12420: [stdlib] Decidable instance for negation | coqbot-app[bot] |
| 2020-11-12 | Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and pop | coqbot-app[bot] |
| 2020-11-12 | Change Dumpglob.pause and Dumpglob.continue into push and pop | Lasse Blaauwbroek |
| 2020-11-12 | Merge PR #13318: Turn ssr proxy notation for supporting second-order/contextu... | coqbot-app[bot] |
| 2020-11-12 | Merge PR #13361: Move last changelog entry for 8.12.1. | coqbot-app[bot] |
| 2020-11-12 | Add changelog entry for Proof using in -noinit mode. | Théo Zimmermann |
| 2020-11-12 | Test case for Proof using in -noinit mode. | Théo Zimmermann |
| 2020-11-12 | Revert to "using" not being a keyword in -noinit mode. | Théo Zimmermann |
| 2020-11-12 | Add support for Proof using in -noinit mode. | Théo Zimmermann |
| 2020-11-12 | Move last changelog entry for 8.12.1. | Théo Zimmermann |
| 2020-11-12 | Merge PR #13359: Print failed test suite logs in CI | coqbot-app[bot] |
| 2020-11-12 | Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no... | coqbot-app[bot] |
| 2020-11-12 | Merge PR #13355: Fix Iris CI script | coqbot-app[bot] |
| 2020-11-12 | Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects. | coqbot-app[bot] |
| 2020-11-12 | Print failed test suite logs in CI | Gaëtan Gilbert |
| 2020-11-12 | Merge the Linked and LinkedInteractive constructors. | Pierre-Marie Pédrot |
| 2020-11-12 | Statically ensure that the native interactive flag is always set to true. | Pierre-Marie Pédrot |
| 2020-11-12 | Statically ensure that native update locations are of form Linked*. | Pierre-Marie Pédrot |
| 2020-11-12 | Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ... | Pierre-Marie Pédrot |
| 2020-11-12 | Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -I | coqbot-app[bot] |
| 2020-11-12 | Add the test as a misc script. | Pierre-Marie Pédrot |
| 2020-11-12 | Add documentation about the soundness bug. | Pierre-Marie Pédrot |
| 2020-11-12 | Fix #13330: Kernel messes with polymorphic side-effects. | Pierre-Marie Pédrot |
| 2020-11-12 | Fix Iris CI script | Gaëtan Gilbert |
| 2020-11-12 | Add changelog for #13345. | Hugo Herbelin |
| 2020-11-12 | Clarifying the role of Add ML Path vs -I (see #13344). | Hugo Herbelin |
| 2020-11-12 | Merge PR #13317: [ssr] intro pattern extensions for dup, swap and apply | coqbot-app[bot] |
| 2020-11-11 | Add changelog for #13351. | Hugo Herbelin |
| 2020-11-11 | Addressing #13349: accept Search on subparts of ident, not only on subidents. | Hugo Herbelin |
| 2020-11-10 | Merge PR #13335: Fix running unit tests with dune compiled coq | coqbot-app[bot] |
| 2020-11-10 | Merge PR #13315: Convert logic chapter to prodn | coqbot-app[bot] |
| 2020-11-10 | Convert logic.rst to prodn | Jim Fehrle |
| 2020-11-10 | Fix running unit tests with dune compiled coq | Gaëtan Gilbert |
| 2020-11-10 | Merge PR #13325: [compat] remove 8.10 | coqbot-app[bot] |
| 2020-11-10 | Merge PR #13322: [obligation] Properly handle no obligations on `Next Obligat... | coqbot-app[bot] |
| 2020-11-10 | Merge PR #13297: Remove the native symbol registering from the safe environment. | coqbot-app[bot] |
| 2020-11-09 | Add additional escape sequences for notations | Jim Fehrle |
| 2020-11-09 | Add global version of OPTINREF | Jim Fehrle |
| 2020-11-09 | Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml... | coqbot-app[bot] |
| 2020-11-09 | Merge PR #13327: Fix documentation of Ltac ::= | coqbot-app[bot] |
| 2020-11-09 | [refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina. | Théo Zimmermann |
