aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2021-01-06Improve description of rewrite_strat/innermost and outermostJim Fehrle
2020-12-30Merge PR #13684: Document the -native-compiler optioncoqbot-app[bot]
2020-12-29[refman] Clarify meaning of goal in documentation of instantiate.Théo Zimmermann
2020-12-29Document the -native-compiler optionPierre Roux
2020-12-21Shorten/improve intro of "Basic proof writing" chapter.Théo Zimmermann
2020-12-14Merge PR #13613: [changes] mark #12765 as experimentalcoqbot-app[bot]
2020-12-14Merge PR #13509: Remove compatibility flag Set Bracketing Last Introduction P...Pierre-Marie Pédrot
2020-12-13Merge PR #13619: doc: Clarify the status of simpl vs cbncoqbot-app[bot]
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
2020-12-11doc: Clarify the status of simpl vs cbnClément Pit-Claudel
2020-12-11Merge PR #13519: Better primitive type support in custom string and numeral n...coqbot-app[bot]
2020-12-11[changes] mark #12765 as experimentalEnrico Tassi
2020-12-11Bump reference to 8.12 refman following unexpected 8.12.2 release.Théo Zimmermann
2020-12-10Changelog for 8.12.2.Théo Zimmermann
2020-12-07Merge PR #13556: Fix spelling in warning entrycoqbot-app[bot]
2020-12-06[doc] update changes after 13501Enrico Tassi
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-12-05Merge PR #13553: Document Number Notation for primitive integerscoqbot-app[bot]
2020-12-04typoYves Bertot
2020-12-04Merge PR #13527: Changes for Coq 8.13coqbot-app[bot]
2020-12-04Better primitive type support in custom string and numeral notations.Fabian Kunze
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-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-02Split long lines in errors and warning indexJim Fehrle
2020-12-02Document Number Notation for primitive integersPierre Roux
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-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-27Improved error message on nested proofsFabian Kunze
2020-11-27Fix #13283: improved error on `clear implicit` flagFabian Kunze
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-24Convert auto chapter to prodnJim Fehrle
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-21Merge PR #12246: Adding support for applying in several hypotheses at the sam...Pierre-Marie Pédrot
2020-11-20Documentation of the support for general single binders in notations.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-02 11:36:24 +0000