aboutsummaryrefslogtreecommitdiff
path: root/doc
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-22Merge PR #14128: Uniformize the name of the Ltac2 boolean equality function.coqbot-app[bot]
2021-04-22Add changelogPierre Roux
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-20Merge PR #14089: unify for Ltac2Pierre-Marie Pédrot
2021-04-19changelog entry for Ltac2 unifySamuel Gruetter
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-17Uniformize the name of the Ltac2 boolean equality function.Pierre-Marie Pédrot
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-17Remove superfluous sort.Jim 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-13Merge PR #14024: [coqdep] error on non-existent and unreadable filescoqbot-app[bot]
2021-04-12[coqdep] error on non-existent and unreadable filesHendrik Tews
2021-04-12Merge PR #14107: Gitignore update for doc_grammar and omega clean-up.coqbot-app[bot]
2021-04-12Remove omega from doc_grammar files.Théo Zimmermann
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-07Merge PR #14008: [stdlib] [Arith] Cantor pairingcoqbot-app[bot]
2021-04-06Merge PR #14077: Add odoc warnings for empty packages.coqbot-app[bot]
2021-04-06Merge PR #13741: Remove omega tactic (deprecated in 8.12)coqbot-app[bot]
2021-04-06Add odoc warnings for empty packages.Théo Zimmermann
2021-04-04Adding change log for #13624.Hugo Herbelin
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-04-02add Cantor pairing to_nat and its inverse of_natAndrej Dudenhefner
2021-04-01Merge PR #14044: [RM] changelog for 8.13.2coqbot-app[bot]
2021-04-01Merge PR #14018: [doc] [coq_makefile] Document that -j N is broken for OCaml ...coqbot-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-30Properly expand projection parameters in Btermdn.Pierre-Marie Pédrot
2021-03-30Remove the :> type castJim Fehrle
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
2021-03-30Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.Pierre-Marie Pédrot
2021-03-30Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers.Michael Soegtrop
2021-03-29[doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0Emilio Jesus Gallego Arias
2021-03-29Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary dependencies:...coqbot-app[bot]
2021-03-29Added a changelog.Pierre-Marie Pédrot
2021-03-26Document as critical.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 06:41:43 +0000