aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-17Merge PR #13007: [build] Don't link `num` anymore in Coqcoqbot-app[bot]
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
2020-09-16Merge PR #8743: [micromega] Switch from `Big_int` to ZArith.BESSON Frederic
2020-09-15[vernac] Don't allow attributes on print / checkEmilio Jesus Gallego Arias
2020-09-15[micromega] Use `minus_one` built-in zarith constant.Emilio Jesus Gallego Arias
2020-09-15[zarith] [micromega] Bump to 1.10 and remove some hacksEmilio Jesus Gallego Arias
2020-09-15Updated .csdp.cache.test-suite and minor fixesBESSON Frederic
2020-09-15[micromega] [test-suite] Update csdp cache for num -> zarith migrationEmilio Jesus Gallego Arias
2020-09-15[micromega] Migrate from num to zarithEmilio Jesus Gallego Arias
2020-09-15[micromega] call csdpcert using path.Emilio Jesus Gallego Arias
2020-09-15Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml"Pierre-Marie Pédrot
2020-09-15Merge PR #12972: [ci] [docker] Up testing to OCaml 4.11.1coqbot-app[bot]
2020-09-14[CI] Always upload artifactsJason Gross
2020-09-14Remove deprecated Extraction Language command value "Ocaml"Jim Fehrle
2020-09-14[nix] Update ref for ocamlformat 0.15Emilio Jesus Gallego Arias
2020-09-14[ocamlformat] Update to ocamlformat 0.15.0Emilio Jesus Gallego Arias
2020-09-14[ci] [docker] Up testing to OCaml 4.11.1Emilio Jesus Gallego Arias
2020-09-14Merge PR #13014: [ci] [mathcomp] run the test suitecoqbot-app[bot]
2020-09-14Merge PR #13022: Fixing documentation relatively to example of use of extra s...coqbot-app[bot]
2020-09-13Fixing documentation relatively to example of use of extra spaces in notations.Hugo Herbelin
2020-09-12Merge PR #12979: Uniformize names for number literals between parsing and refmancoqbot-app[bot]
2020-09-11[numeral notation] Improve documentationPierre Roux
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
2020-09-11Adding a wit_natural standard argument.Hugo Herbelin
2020-09-11Turn integer into natural in several mlgsPierre Roux
2020-09-11[refman] Explicit integer and naturalPierre Roux
2020-09-11[refman] Rename int to integerPierre Roux
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-03 01:09:29 +0000