aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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
2020-09-18Make `simple apply in ...` point to `simple apply`Maxime Dénès
2020-09-18[ci] [dmesg] save as artifactEnrico Tassi
2020-09-18Improve `simple apply` exampleMaxime Dénès
2020-09-18Merge PR #12610: [leminv] [declare] Use higher-level Declare API.Pierre-Marie Pédrot
2020-09-18Remove unused API from Dn.Pierre-Marie Pédrot
2020-09-18Clean up a bit the implemenation of dnets.Pierre-Marie Pédrot
2020-09-18Remove dead code in dnets.Pierre-Marie Pédrot
2020-09-18Merge PR #13027: [vernac] Don't allow attributes on print / checkcoqbot-app[bot]
2020-09-17[ci/gitlab/cachix] Avoid running in trouble when calling git fetch --unshallow.Théo Zimmermann
2020-09-17Merge PR #13007: [build] Don't link `num` anymore in Coqcoqbot-app[bot]
2020-09-17[configure] Fix version checks for lablgtk and zarithEmilio Jesus Gallego Arias
2020-09-17Be more efficient when generating the merge of ltle maps in AcyclicGraph.Pierre-Marie Pédrot
2020-09-17Do not allocate intermediate sets in universe refreshing.Pierre-Marie Pédrot
2020-09-17[leminv] Use higher-level Declare API.Emilio Jesus Gallego Arias
2020-09-17[leminv] Remove unused catch.Emilio Jesus Gallego Arias
2020-09-17[install] Rewording of primitive floats.Emilio Jesus Gallego Arias
2020-09-17[build] Don't link `num` anymore in CoqEmilio Jesus Gallego Arias
2020-09-17Merge PR #13024: [CI] Always upload artifactscoqbot-app[bot]
2020-09-17[ci] call dmesg after quick/async jobs to detect OOMEnrico Tassi
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
2020-09-16Merge PR #13008: Use fresher names in eqschemesHugo Herbelin
2020-09-16Merge PR #13015: Propagate zarith dependency.Vincent Laporte