aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/extensions
AgeCommit message (Expand)Author
2021-04-22Extend Canonical Structure documentation.Jan-Oliver Kaiser
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-04typoYves Bertot
2020-11-27Fix #13283: improved error on `clear implicit` flagFabian Kunze
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-18Review commit: improving the doc of boolean attributes.Théo Zimmermann
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
2020-11-14Move destructuring let syntax closer to its documentation.Théo Zimmermann
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
2020-11-03improved documentation of arguments commandFabian Kunze
2020-11-02Doc: added "Arguments" removing implicit argumentsFabian Kunze
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all patter...coqbot-app[bot]
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-05Documenting warning about unused variables in pattern clauses.Hugo Herbelin
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-09-11[refman] Rename num to naturalPierre Roux
2020-09-08Update doc/sphinx/language/extensions/match.rstClément Blaudeau
2020-09-08[Small typo] Update match.rstClément Blaudeau
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-08-06Trying to rephrase complex sentences to make them easier to read.Martin Bodin
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
2020-05-15Document new Search features.Théo Zimmermann
2020-05-15Fix typo.Théo Zimmermann
2020-05-14Fix title level and a build failure.Théo Zimmermann
2020-05-14Add some markers of origin.Théo Zimmermann
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-14Refactoring of the first part of the reference manual.Théo Zimmermann
2020-05-14Preserve Implicit arguments file.Théo Zimmermann
2020-05-14Remove Canonical structures from Implicit arguments.Théo Zimmermann
2020-05-14Merge doc on Canonical structures from two origins.Théo Zimmermann
2020-05-14Move Canonical structures file into new location.Théo Zimmermann
2020-05-14Add Canonical structure declarations to Canonical structures file.Théo Zimmermann
2020-05-14Extract Canonical structures from Implicit arguments.Théo Zimmermann
2020-05-14Split Gallina extensions into multiple files.Théo Zimmermann
2020-05-14Merge doc on extended pattern matching from two origins.Théo Zimmermann
2020-05-14Move extended pattern matching to new location.Théo Zimmermann
2020-05-13Add section on pattern matching from Gallina ext.Théo Zimmermann
2020-05-13New file on existential variables.Théo Zimmermann
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-03Move section on implicit arguments in appropriate location (inside extensions).Théo Zimmermann
2020-03-19Adapt to sub-TOC not showing in PDF output.Théo Zimmermann
2020-03-19[refman] Move chapters into new structure.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:35:37 +0000