aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Expand)Author
2021-04-23Merge PR #14041: Enable canonical fun _ => _ projections.coqbot-app[bot]
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
2021-04-22Extend Canonical Structure documentation.Jan-Oliver Kaiser
2021-04-21Merge PR #14094: Properly pass the Ltac2 notation level to the gramlib API.coqbot-app[bot]
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
2021-04-19Merge PR #14108: [zify] bugfixVincent Laporte
2021-04-19Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in Sphi...coqbot-app[bot]
2021-04-19Merge PR #13815: Improve description of conversionscoqbot-app[bot]
2021-04-17Improve conversion chapter.Jim Fehrle
2021-04-17Disambiguate move tactics.Jim Fehrle
2021-04-17Include (* ... *) comments in .. coqtop:: directives in Sphinx outputJim Fehrle
2021-04-17Properly pass the Ltac2 notation level to the gramlib API.Pierre-Marie Pédrot
2021-04-16[zify] bugfixFrederic Besson
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
2021-04-10Merge PR #14091: Fix link in doc/cic.rst, there is no Credits chapter anymorecoqbot-app[bot]
2021-04-10Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on red/or...coqbot-app[bot]
2021-04-10Fix link in doc/cic.rst, there is no Credits chapter anymoreYannick Forster
2021-04-08Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.Pierre-Marie Pédrot
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-01Merge PR #14044: [RM] changelog for 8.13.2coqbot-app[bot]
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
2021-04-01changelog for 8.13.2Enrico Tassi
2021-03-30Remove the :> type castJim Fehrle
2021-03-29[doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0Emilio Jesus Gallego Arias
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and notat...Michael Soegtrop
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
2021-03-13Documenting the changes.Pierre-Marie Pédrot
2021-03-10Merge PR #13840: [notation] option to fine tune printing of literalscoqbot-app[bot]
2021-03-10Add documentation.Pierre-Marie Pédrot
2021-03-10Regenerate the Ltac2 syntax for documentation.Pierre-Marie Pédrot
2021-03-08Merge PR #13707: Convert 2nd part of rewriting chapter to prodncoqbot-app[bot]
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-05Merge PR #13842: Remove decimal-only number notations (deprecated in 8.12)Pierre-Marie Pédrot
2021-03-04doc: don't count a contributor twice in the changelogLi-yao Xia
2021-03-04[doc] Set/Unset Printing Raw LiteralsEnrico Tassi
2021-03-02Merge PR #13889: Dead code elimination: not reducible error message is never ...coqbot-app[bot]
2021-03-02Dead code elimination: not reducible error message is never raised.Théo Zimmermann
2021-02-28Fix link of default_bindings.slb Prime
2021-02-27Remove decimal-only number notationsPierre Roux
2021-02-26Signed primitive integersAna
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-02-22mention --version to CoqIDEEnrico Tassi
2021-02-22changelog for 8.13.1Enrico Tassi
2021-02-14Show "Error:"/"Warning:" with white type (on red/orange background)Jim Fehrle
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-28Merge PR #13799: Replace : term with : type in open binders.coqbot-app[bot]
2021-01-28Merge PR #13789: Document limitation of rewrite regarding occurrence selection.coqbot-app[bot]
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:05:22 +0000