aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-09-30Remove the forward class hint feature.Pierre-Marie Pédrot
2020-09-29Merge PR #13111: Small document fixes.coqbot-app[bot]
2020-09-30Wf.v defines Fix_eq, not fix_eq.Tanaka Akira
2020-09-30Type{i} should be Type(i).Tanaka Akira
2020-09-29Merge PR #13101: Reduce nitpick_ignore list a little.Clément Pit-Claudel
2020-09-29Merge PR #13097: Modify how quotations handle whole sentences.coqbot-app[bot]
2020-09-29Merge PR #13039: Lint stdlib with -mangle-names #3coqbot-app[bot]
2020-09-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lon...coqbot-app[bot]
2020-09-28Merge PR #13105: [nix] CI script wrapper now requires Pythoncoqbot-app[bot]
2020-09-28Merge PR #13053: [lib] make canonical_path_name always absolute (fix #13031)Pierre-Marie Pédrot
2020-09-28CI script wrapper now requires PythonMaxime Dénès
2020-09-27Avoid lookup up too many characters.Guillaume Melquiond
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-09-27Recognize only ":{{" as a sentence-gobbling quotation.Guillaume Melquiond
2020-09-27Make "xxx:{{" always start a quotation, whether registered or not.Guillaume Melquiond
2020-09-25Merge PR #12999: More improvements in locating tactic errorscoqbot-app[bot]
2020-09-24Merge PR #12894: Modify bytecode representation of closures to please OCamls ...coqbot-app[bot]
2020-09-24Merge PR #13077: Fix issue #13065 - Windows CI brokencoqbot-app[bot]
2020-09-23Fix issue #13065 - Windows CI brokenMichael Soegtrop
2020-09-23Merge PR #12977: Statically ensure that only polymophic hint terms come with ...coqbot-app[bot]
2020-09-23Merge PR #13073: A temporary fix of #13018 and #12775 for branch 8.12 (bis)coqbot-app[bot]
2020-09-23Merge PR #13028: Fixes #9716 and #13004: don't drop the qualifier of quotatio...Pierre-Marie Pédrot
2020-09-23Merge PR #12847: Tactics inversion and replace work with eq in typePierre-Marie Pédrot
2020-09-22Merge PR #13061: fix build:quick and build:base+async artifactscoqbot-app[bot]
2020-09-22Merge PR #13067: Setting default value for Display Parentheses off in CoqIDEcoqbot-app[bot]
2020-09-22Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested applica...coqbot-app[bot]
2020-09-22Adding change log for #12794 and #13067.Hugo Herbelin
2020-09-22Setting default value for Display Parentheses off in CoqIDE.Hugo Herbelin
2020-09-22Add overlay for Equations.Hugo Herbelin
2020-09-22Adding change log for #13028.Hugo Herbelin
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-22Use the closure tag for accumulators.Guillaume Melquiond
2020-09-22Use the same memory layout as closures for accumulators.Guillaume Melquiond
2020-09-22Modify bytecode representation of closures to please OCaml's GC (fix #12636).Guillaume Melquiond
2020-09-22Merge PR #13046: Small optimization of acyclic graph merge operationcoqbot-app[bot]
2020-09-22Merge PR #13050: [ci/gitlab/cachix] Avoid running in trouble when calling git...coqbot-app[bot]
2020-09-22Merge PR #13049: [configure] Fix version checks for lablgtk and zarithcoqbot-app[bot]
2020-09-22Merge PR #13063: Make print-pretty-timed robust against non-output-sync logscoqbot-app[bot]
2020-09-21Merge PR #13057: Adding debugging printers for Intmapcoqbot-app[bot]
2020-09-21Make print-pretty-timed robust against non-output-sync logsJason Gross
2020-09-21Bump nixpkgs to get zarith 1.10.Théo Zimmermann
2020-09-21Merge PR #12723: dune: pass -bin-annot to configurecoqbot-app[bot]
2020-09-21fix build:quick and build:base+async artifactsGaëtan Gilbert
2020-09-19Merge PR #13052: Clean up Dnet implementationHugo Herbelin
2020-09-18Merge PR #13055: Fix Removed in Sphinx 4 deprecations.coqbot-app[bot]
2020-09-18Merge PR #12963: Formally deprecate the double induction tactic.Hugo Herbelin
2020-09-18Adding debugging printers for Intmap.Hugo Herbelin
2020-09-18Merge PR #13051: Improve `simple apply` examplecoqbot-app[bot]
2020-09-18Merge PR #13043: [ci] call dmesg after quick/async jobs to detect OOMcoqbot-app[bot]
2020-09-18Fix Removed in Sphinx 4 deprecations.Théo Zimmermann