aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
AgeCommit message (Expand)Author
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
2021-04-22Extend Canonical Structure documentation.Jan-Oliver Kaiser
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
2021-04-19Merge PR #13815: Improve description of conversionscoqbot-app[bot]
2021-04-17Improve conversion chapter.Jim Fehrle
2021-04-10Fix link in doc/cic.rst, there is no Credits chapter anymoreYannick Forster
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-04typoYves Bertot
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-27Merge PR #13483: Fix #13283: improved error on `clear implicit` flagcoqbot-app[bot]
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-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-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-03Merge PR #13293: Doc: added "Arguments" removing implicit argumentscoqbot-app[bot]
2020-11-03improved documentation of arguments commandFabian Kunze
2020-11-02Doc: added "Arguments" removing implicit argumentsFabian Kunze
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-26Merge PR #12768: Granting wish #12762: warning on duplicated catch-all patter...coqbot-app[bot]
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-05Documenting warning about unused variables in pattern clauses.Hugo Herbelin
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-29Merge PR #13111: Small document fixes.coqbot-app[bot]
2020-09-30Wf.v defines Fix_eq, not fix_eq.Tanaka Akira
2020-09-30Type{i} should be Type(i).Tanaka Akira
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:59:15 +0000