aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language/core
AgeCommit message (Expand)Author
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
2021-04-17Improve conversion chapter.Jim Fehrle
2021-03-30Remove the :> type castJim Fehrle
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-02-26Signed primitive integersAna
2021-02-08Properly document the local and global locality attributes.Théo Zimmermann
2021-02-05Fix hierarchy of sections in module chapter.Théo Zimmermann
2021-01-28Replace : term with : type in open binders.Théo Zimmermann
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-03[refman] Fix error names.Théo Zimmermann
2020-11-27Merge PR #12586: [declare] Allow custom typing flags when declaring constants.coqbot-app[bot]
2020-11-27Improved error message on nested proofsFabian 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-18Review commit: improving the doc of boolean attributes.Théo Zimmermann
2020-11-18Run doc_grammar for #13312.Théo Zimmermann
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
2020-11-16Update grammar in docJim Fehrle
2020-11-16Doc for variance syntaxGaëtan Gilbert
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-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
2020-11-02[doc] attribute #[using]Enrico Tassi
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-25Merge PR #12936: Convert misc chapters to prodn, update syntaxcoqbot-app[bot]
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-23Correct doc using :>>Gaëtan Gilbert
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-12Add missing ";" in record grammarJim Fehrle
2020-10-05Document the removal of forward class hints.Théo Zimmermann
2020-10-02More details in the documentation of native arraysVincent Semeria
2020-09-11[numeral notation] Improve documentationPierre Roux
2020-09-11[refman] Explicit integer and naturalPierre Roux
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename numeral to numberPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
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-15Document semantic restriction on patternsJim Fehrle
2020-07-06Primitive persistent arraysMaxime Dénès
2020-06-09Merge sections on functions and function types.Théo Zimmermann
2020-06-09Minor improvements to the section on sorts.Théo Zimmermann
2020-06-09Minor improvements to the section on basics.Théo Zimmermann
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-27Changelog entries for the 8.12 changes to the reference manual.Théo Zimmermann
2020-05-18Use the new gdef alt-text feature in the refman.Théo Zimmermann
2020-05-15Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into mul...Clément Pit-Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:30:30 +0000