aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
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-28Merge PR #12946: Fixes part 1 of #12908: undetected collision involving a lon...coqbot-app[bot]
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
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 #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-22Adding change log for #13028.Hugo Herbelin
2020-09-21Make print-pretty-timed robust against non-output-sync logsJason Gross
2020-09-18Merge PR #13055: Fix Removed in Sphinx 4 deprecations.coqbot-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-18Improve `simple apply` exampleMaxime Dénès
2020-09-17[build] Don't link `num` anymore in CoqEmilio Jesus Gallego Arias
2020-09-15Adding change log for #13026.Hugo Herbelin
2020-09-15Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml"Pierre-Marie Pédrot
2020-09-14Remove deprecated Extraction Language command value "Ocaml"Jim Fehrle
2020-09-14[ci] [docker] Up testing to OCaml 4.11.1Emilio Jesus Gallego Arias
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-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
2020-09-11[refman] Rename numeral to numberPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-09-11[parsing] Simplify bigintPierre Roux
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-09-11[refman] Replace num by intPierre Roux
2020-09-11Remove outdated references to productionlist.Théo Zimmermann
2020-09-11Minimal changes to make the refman compatible with Sphinx 3.Théo Zimmermann
2020-09-10Merge PR #12998: changelog entry for 12857coqbot-app[bot]
2020-09-10Update doc/changelog/06-ssreflect/12857-changelog-for-12857.rstEnrico Tassi
2020-09-09Merge PR #12994: Fix docgram's dune file following #12085.coqbot-app[bot]
2020-09-09Merge PR #12094: Extend app_inj_tail and other list lemmasHugo Herbelin
2020-09-09changelog entry for 12857Enrico Tassi
2020-09-09Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable fro...Pierre-Marie Pédrot
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
2020-09-08Fix docgram's dune file following #12085.Théo Zimmermann
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type i...coqbot-app[bot]
2020-09-08Update doc/sphinx/language/extensions/match.rstClément Blaudeau
2020-09-08[Small typo] Update match.rstClément Blaudeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:28:22 +0000