aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/extensions/match.rst
AgeCommit message (Collapse)Author
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
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
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-10-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all ↵coqbot-app[bot]
pattern-matching clause with unused named variable Reviewed-by: jfehrle Reviewed-by: vbgl Ack-by: gares
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-05Documenting warning about unused variables in pattern clauses.Hugo Herbelin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-09-11[refman] Rename num to naturalPierre Roux
2020-09-08Update doc/sphinx/language/extensions/match.rstClément Blaudeau
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-09-08[Small typo] Update match.rstClément Blaudeau
Some error messages were merged together
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-06-08Convert Ltac chapter to prodnJim Fehrle
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-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