aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-11-15Adding change log for #12685.Hugo Herbelin
2020-11-15Propagating scope information in indirect application to a reference.Hugo Herbelin
2020-11-15Merge PR #13339: In -noinit mode, add support for Proof using, using is not a...Pierre-Marie Pédrot
2020-11-15Merge PR #13350: Fix incorrect "avoid" set in globenv extra dataPierre-Marie Pédrot
2020-11-15Merge PR #13356: Make the universe of primitive arrays irrelevantPierre-Marie Pédrot
2020-11-14Coqdoc: we move a newline at a better place.Hugo Herbelin
2020-11-14Documenting one-line verbatim.Hugo Herbelin
2020-11-14Addressing #13304: how to verbatim an expression mentioning >>.Hugo Herbelin
2020-11-14Merge PR #13369: Move destructuring let syntax closer to its documentation.coqbot-app[bot]
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-14Dead code in coqdoc.Hugo Herbelin
2020-11-14Reorganizing the printing of warnings; fixing line count.Hugo Herbelin
2020-11-14Move destructuring let syntax closer to its documentation.Théo Zimmermann
2020-11-14Add changelog for #13376.Hugo Herbelin
2020-11-14Avoiding encapsulating exceptions w/o a handler in NotFoundInstance.Hugo Herbelin
2020-11-13Add changelog for #13373.Hugo Herbelin
2020-11-13Fixes #13363: case of a meta not paying attention to being under binders.Hugo Herbelin
2020-11-13[record] Some documentation + minor refactoringEmilio Jesus Gallego Arias
2020-11-13[record] [ci] Overlay for elpiEmilio Jesus Gallego Arias
2020-11-13[record] Options API cleanup.Emilio Jesus Gallego Arias
2020-11-13[record] Refactor nested functions.Emilio Jesus Gallego Arias
2020-11-13[record] Cleanup of data structure and functions [2/2]Emilio Jesus Gallego Arias
2020-11-13[record] Cleanup of data structure and functions [1/2]Emilio Jesus Gallego Arias
2020-11-13Merge PR #13358: Merge the Linked / LinkedInteractive native link information...coqbot-app[bot]
2020-11-13Hardcode next_up and next_down instead of relying on nextafter.Guillaume Melquiond
2020-11-13Add allocation-free variants of the nextup and nextdown floating-point operat...Guillaume Melquiond
2020-11-13Remove floating-point comparison operators as they are no longer needed.Guillaume Melquiond
2020-11-13Turn coq_float64.h into a .c file as it is no longer needed by coq_interp.c.Guillaume Melquiond
2020-11-13Inline the functions from coq_float64.h.Guillaume Melquiond
2020-11-13Make callback opcodes more generic.Guillaume Melquiond
2020-11-13Optimize Is_accu a bit.Guillaume Melquiond
2020-11-13Improve documentation of closure representations.Guillaume Melquiond
2020-11-13Turn Ksequence into a unary opcode, as its binary structure was never used.Guillaume Melquiond
2020-11-13Remove unused if-then-else construct from VM.Guillaume Melquiond
2020-11-13Restore discard_dead_code and use it to simplify match-with constructs.Guillaume Melquiond
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 19:20:18 +0000