aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2021-02-25Merge PR #13202: Infrastructure for fine-grained debug flagscoqbot-app[bot]
2021-02-25Merge PR #13863: Get rid of the compilation date from the binaries to make th...coqbot-app[bot]
2021-02-25Merge PR #13080: Ascii: add leb and ltbcoqbot-app[bot]
2021-02-25Merge PR #13738: Make sure Ltac2 get cleaned too.coqbot-app[bot]
2021-02-24Overlay for Set DebugGaëtan Gilbert
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-23Print anomaly labels regardless of -debug, and never print user_err labelsGaëtan Gilbert
2021-02-23Merge PR #13880: Fix the release process checklist with respect to the refman...coqbot-app[bot]
2021-02-22Fix the release process checklist with respect to the refman update.Théo Zimmermann
2021-02-22Merge PR #13878: [RM] Changelog for 8.13.1coqbot-app[bot]
2021-02-22Merge PR #13836: Make detyping more resistent in the debuggerPierre-Marie Pédrot
2021-02-22Merge PR #13828: Fix doc comment in pp.mlicoqbot-app[bot]
2021-02-22mention --version to CoqIDEEnrico Tassi
2021-02-22Merge PR #13872: Make lemmas from Reals opaque whenever possible.coqbot-app[bot]
2021-02-22Merge PR #13870: Add option --version to Coqide (fix #13752).coqbot-app[bot]
2021-02-22changelog for 8.13.1Enrico Tassi
2021-02-20Merge PR #13874: add changelog for #13867 (Fix missing arities of VM opcodes)coqbot-app[bot]
2021-02-20Update doc/changelog/01-kernel/13867-changelog-for-13867.rstEnrico Tassi
2021-02-20add changelog for 13867Enrico Tassi
2021-02-20Inline proofs of exist_exp0 and exist_cos0.Guillaume Melquiond
2021-02-19Remove some trivial definition.Guillaume Melquiond
2021-02-19Abstract the non-computational part away.Guillaume Melquiond
2021-02-19Terminate intermediate lemmas with Qed.Guillaume Melquiond
2021-02-19Make intermediate lemmas more explicit, so that they can be terminated by Qed.Guillaume Melquiond
2021-02-19Make most of DRealAbstr opaque.Guillaume Melquiond
2021-02-19Terminate some lemmas with Qed.Guillaume Melquiond
2021-02-19Merge PR #13865: [coqtop] be verbose only in interactive modecoqbot-app[bot]
2021-02-19Be less permissive with respect to nonsensical bytecode.Guillaume Melquiond
2021-02-19Make the generated file the official source of arity.Guillaume Melquiond
2021-02-19Add a file coq_arity.h generated by genOpcodeFiles.ml.Guillaume Melquiond
2021-02-19Merge PR #13867: Fix missing arities of VM opcodes.Pierre-Marie Pédrot
2021-02-17Add option --version to Coqide (fix #13752).Guillaume Melquiond
2021-02-17Use make_case_or_project in auto_ind_declGaëtan Gilbert
2021-02-17Reduce imperative arrays in build_beq_scheme + reindentGaëtan Gilbert
2021-02-17Merge PR #13734: Fix #13732: Implicit Type vs universesPierre-Marie Pédrot
2021-02-17Add an entry to file critical-bugs.Guillaume Melquiond
2021-02-16Fix missing arities of VM opcodes.Guillaume Melquiond
2021-02-16Merge PR #13866: Only run windows job when WINDOWS=enabledcoqbot-app[bot]
2021-02-16[coqtop] be verbose only in interactive modeEnrico Tassi
2021-02-16Only run windows job when WINDOWS=enabledGaëtan Gilbert
2021-02-16Get rid of the compilation date from the binaries to make them more stable.Guillaume Melquiond
2021-02-15Fix doc comment in pp.mliGaëtan Gilbert
2021-02-11Merge PR #13844: [vernac] pass the loc of the whole command to the interp fun...coqbot-app[bot]
2021-02-11[ci] overlay for elpiEnrico Tassi
2021-02-11Merge PR #13640: Add ounit2 to with-test dependenciescoqbot-app[bot]
2021-02-11Merge PR #13642: Add build dependency of conf-python-3 to coq-doccoqbot-app[bot]
2021-02-11Merge PR #13823: Update release process following coq/ceps#52.coqbot-app[bot]
2021-02-11Merge PR #13831: Properly document the local and global locality attributes.coqbot-app[bot]
2021-02-11[vernac] pass the loc of the whole command to the interp functionEnrico Tassi
2021-02-11Merge PR #13847: [ci] elpi 1.13.0coqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 14:24:49 +0000