aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-14Show "Error:"/"Warning:" with white type (on red/orange background)Jim Fehrle
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]
2021-02-11overlay for coq-elpiEnrico Tassi
2021-02-11[ci] elpi 1.13.0Enrico Tassi
2021-02-11Merge PR #13826: [micromega] Fixes #13794Vincent Laporte
2021-02-10Merge PR #13818: [bench] Re-enable coq-performance-testscoqbot-app[bot]
2021-02-10Merge PR #13821: Properly handle ordering of -w and -native-compilercoqbot-app[bot]
2021-02-10[micromega/nia] Improve sharing of proofsBESSON Frederic
2021-02-09Merge PR #13822: Remove deprecated command line argumentscoqbot-app[bot]
2021-02-09Merge PR #13810: ide: shift+enter to find backwardscoqbot-app[bot]
2021-02-08Properly document the local and global locality attributes.Théo Zimmermann
2021-02-08Make detyping more resistent in the debuggerGaëtan Gilbert
2021-02-06Merge PR #13829: Fix hierarchy of sections in module chapter.coqbot-app[bot]
2021-02-05Fix hierarchy of sections in module chapter.Théo Zimmermann
2021-02-04Update release process following coq/ceps#52.Théo Zimmermann
2021-02-04Changelog for #13822Gaëtan Gilbert
2021-02-04Remove deprecated -inputstate command line argumentGaëtan Gilbert
2021-02-04Remove deprecated -sprop-cumulative command line argumentGaëtan Gilbert
2021-02-04Merge PR #13731: vernac/declaremods: make object collection tail-recursivecoqbot-app[bot]
2021-02-04Properly handle ordering of -w and -native-compilerGaëtan Gilbert
2021-02-04Merge PR #13528: [RM] Script to list the contributors between two git revisionscoqbot-app[bot]
2021-02-04Use release branch instead of master.Théo Zimmermann
2021-02-03Merge PR #13817: CI: Switch coqhammer job to edge ocamlcoqbot-app[bot]
2021-02-03Merge PR #13776: Fix #13739 - disable some warnings when calling Function.coqbot-app[bot]
2021-02-03Fix #13739 - disable some warnings when calling Function.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 05:04:22 +0000