aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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[lib] make canonical_path_name always absolute (fix #13031)Enrico Tassi
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-16Modify setoid_ring/BinList.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Lists/List.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify setoid_ring/Ring_theory.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify NArith/Nnat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify PArith/Pnat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify NArith/BinNat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify PArith/BinPos.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Wf_nat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/EqNat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Factorial.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Compare_dec.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Peano_dec.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Logic/Eqdep_dec.v to compile with -vJasper Hugunin
2020-09-16Modify Logic/EqdepFacts.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Between.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Mult.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Plus.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/Le.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Arith/PeanoNat.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NBits.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NLcm.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NGcd.v to compile with -mangle-namesJasper Hugunin
2020-09-16Modify Numbers/Natural/Abstract/NDiv.v to compile with -mangle-namesJasper Hugunin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 17:45:26 +0000