aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2020-12-03Implement review corrections by Théo ZimmermannMatthieu Sozeau
2020-12-03Implement suggestions by Théo ZimmermannMatthieu Sozeau
2020-12-03Apply suggestions from code reviewMatthieu Sozeau
2020-12-03Apply suggestions from code reviewEnrico Tassi
2020-12-03Update doc/sphinx/changes.rstMatthieu Sozeau
2020-12-03Fixes in the summary by Jim FehrleMatthieu Sozeau
2020-12-03Changes without PR references fixesMatthieu Sozeau
2020-12-03Apply suggestions from @jfehrle code reviewMatthieu Sozeau
2020-12-03[changelog] update markupEnrico Tassi
2020-12-03Add an anchor in syntax-extensionsMatthieu Sozeau
2020-12-03Changes for Coq 8.13Matthieu Sozeau
2020-12-03[refman] Fix error names.Théo Zimmermann
2020-12-03Merge PR #13554: Split long lines in errors and warning indexcoqbot-app[bot]
2020-12-02Split long lines in errors and warning indexJim Fehrle
2020-12-02Merge PR #13275: Put all Int63 primitives in a separate fileVincent Laporte
2020-12-02Document Number Notation for primitive integersPierre Roux
2020-12-02Put all Int63 primitives in a separate filePierre Roux
2020-12-01Merge PR #13490: [ssr] Backport ssrbool from MathComp 1.12.0coqbot-app[bot]
2020-11-30Adding a changelog for Ltac1.lambda.Pierre-Marie Pédrot
2020-11-30Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumu...coqbot-app[bot]
2020-11-29Backport ssrbool lemmas from MathComp 1.12.0Kazuhiko Sakaguchi
2020-11-28Merge PR #13496: Revert "Remove deprecated tactic cutrewrite."coqbot-app[bot]
2020-11-27Merge PR #12586: [declare] Allow custom typing flags when declaring constants.coqbot-app[bot]
2020-11-27[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ...Matthieu Sozeau
2020-11-27Merge PR #13483: Fix #13283: improved error on `clear implicit` flagcoqbot-app[bot]
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
2020-11-27Merge PR #13482: Improved error message on nested proofscoqbot-app[bot]
2020-11-27Merge PR #13473: Testing {in _, _} and {pred _} from ssrboolcoqbot-app[bot]
2020-11-27Improved error message on nested proofsFabian Kunze
2020-11-27Fix #13283: improved error on `clear implicit` flagFabian Kunze
2020-11-27Merge PR #13457: [RM] Update magicno & compatcoqbot-app[bot]
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
2020-11-26[declare] Allow custom typing flags when declaring constants.Emilio Jesus Gallego Arias
2020-11-25Testing {in _, _} and {pred _} from ssrboolCyril Cohen
2020-11-25Changelog for #13415Gaëtan Gilbert
2020-11-25Merge PR #13459: [ssr] Fixing [dup] and [swap] working around a bugcoqbot-app[bot]
2020-11-25Merge PR #13405: Alternative implementation of the Micromega persistent cacheVincent Laporte
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-24Add a changelog.Pierre-Marie Pédrot
2020-11-24Fixing [dup] and [swap]Cyril Cohen
2020-11-23Add COPYALL and APPENDALL edit ops, drop unneeded codeJim Fehrle
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notat...coqbot-app[bot]
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make s...coqbot-app[bot]
2020-11-22Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".Hugo Herbelin
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the sam...Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:25:33 +0000