aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-13Remove some unused opcodes from VM.Guillaume Melquiond
2020-11-13Remove unchecked arithmetic operations from VM, as they are not used.Guillaume Melquiond
2020-11-13Optimize handling of the VM stack with respect to the GC.Guillaume Melquiond
2020-11-13Fix incorrect "avoid" set in globenv extra dataGaëtan Gilbert
2020-11-13Make the universe of primitive arrays irrelevantGaëtan Gilbert
2020-11-13Remove unused CClosure.FNativeEntries.farrayGaëtan Gilbert
2020-11-13Fix dune rules for @check-gram following recent changes.Théo Zimmermann
2020-11-13Merge PR #12420: [stdlib] Decidable instance for negationcoqbot-app[bot]
2020-11-13Add changelog for #13365Li-yao Xia
2020-11-13Fix proof of Coq.Program.Wf.Fix_F_inv to be axiom-freeLi-yao Xia
2020-11-12Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and popcoqbot-app[bot]
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
2020-11-12Merge PR #13318: Turn ssr proxy notation for supporting second-order/contextu...coqbot-app[bot]
2020-11-12Merge PR #13361: Move last changelog entry for 8.12.1.coqbot-app[bot]
2020-11-12Add changelog entry for Proof using in -noinit mode.Théo Zimmermann
2020-11-12Test case for Proof using in -noinit mode.Théo Zimmermann
2020-11-12Revert to "using" not being a keyword in -noinit mode.Théo Zimmermann
2020-11-12Add support for Proof using in -noinit mode.Théo Zimmermann
2020-11-12Move last changelog entry for 8.12.1.Théo Zimmermann
2020-11-12Merge PR #13359: Print failed test suite logs in CIcoqbot-app[bot]
2020-11-12Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no...coqbot-app[bot]
2020-11-12Merge PR #13355: Fix Iris CI scriptcoqbot-app[bot]
2020-11-12Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects.coqbot-app[bot]
2020-11-12Print failed test suite logs in CIGaëtan Gilbert
2020-11-12Merge the Linked and LinkedInteractive constructors.Pierre-Marie Pédrot
2020-11-12Statically ensure that the native interactive flag is always set to true.Pierre-Marie Pédrot
2020-11-12Statically ensure that native update locations are of form Linked*.Pierre-Marie Pédrot
2020-11-12Merge PR #13289: Cosmetic cleaning of uState.ml: a bit of doc, more unity in ...Pierre-Marie Pédrot
2020-11-12Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -Icoqbot-app[bot]
2020-11-12Add the test as a misc script.Pierre-Marie Pédrot
2020-11-12Add documentation about the soundness bug.Pierre-Marie Pédrot
2020-11-12Fix #13330: Kernel messes with polymorphic side-effects.Pierre-Marie Pédrot
2020-11-12Fix Iris CI scriptGaëtan Gilbert
2020-11-12Add changelog for #13345.Hugo Herbelin
2020-11-12Clarifying the role of Add ML Path vs -I (see #13344).Hugo Herbelin
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
2020-11-11We move the example of Makefile wrapper next to the explanations about CoqMak...Hugo Herbelin
2020-11-11Add changelog for #13351.Hugo Herbelin
2020-11-11Addressing #13349: accept Search on subparts of ident, not only on subidents.Hugo Herbelin
2020-11-10Merge PR #13335: Fix running unit tests with dune compiled coqcoqbot-app[bot]
2020-11-10Merge PR #13315: Convert logic chapter to prodncoqbot-app[bot]
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-10Fix running unit tests with dune compiled coqGaëtan Gilbert
2020-11-10Merge PR #13325: [compat] remove 8.10coqbot-app[bot]
2020-11-10Merge PR #13322: [obligation] Properly handle no obligations on `Next Obligat...coqbot-app[bot]
2020-11-10Merge PR #13297: Remove the native symbol registering from the safe environment.coqbot-app[bot]
2020-11-09Add additional escape sequences for notationsJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-11-09Merge PR #13329: [refman] Stop applying a special style to Coq, CoqIDE, OCaml...coqbot-app[bot]
2020-11-09Merge PR #13327: Fix documentation of Ltac ::=coqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 10:48:09 +0000