aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2020-12-01Merge PR #13490: [ssr] Backport ssrbool from MathComp 1.12.0coqbot-app[bot]
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
2020-11-20Merge PR #13265: Add support for general non-necessarily-recursive binders in...coqbot-app[bot]
2020-11-20Merge PR #13352: Configure default value of -native-compilercoqbot-app[bot]
2020-11-20Add changelog for #13265.Hugo Herbelin
2020-11-20Documentation of the support for general single binders in notations.Hugo Herbelin
2020-11-20Add changelogPierre Roux
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions b...coqbot-app[bot]
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Adding change log.Hugo Herbelin
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
2020-11-20Update doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars...Hugo Herbelin
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a primiti...coqbot-app[bot]
2020-11-19Adding changelog for #13237.Hugo Herbelin
2020-11-19Merge PR #13423: [changelog] Indicate a replacement for deprecated syntax of ...coqbot-app[bot]
2020-11-19[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto.Théo Zimmermann
2020-11-19Add changelog for #13386.Hugo Herbelin
2020-11-19Fix typo in rst link syntax.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:31:39 +0000