aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2021-04-19Merge PR #13846: Include (* ... *) comments in .. coqtop:: directives in ↵coqbot-app[bot]
Sphinx output Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2021-04-19Merge PR #13815: Improve description of conversionscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
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
Removing it makes no difference to the order of glossary entries, which is determined by the "for ... sorted" statement above.
2021-04-16Merge PR #13939: Allow scope delimiters in Ltac2 open_constr:(...) quotation.coqbot-app[bot]
Reviewed-by: JasonGross
2021-04-13Merge PR #14024: [coqdep] error on non-existent and unreadable filescoqbot-app[bot]
Reviewed-by: gares Ack-by: jfehrle Ack-by: ejgallego
2021-04-12[coqdep] error on non-existent and unreadable filesHendrik Tews
Print an error message and return non-zero status for non-existing or unreadable files. Unknown options produce a warning and are otherwise ignored. Fixes #14023
2021-04-12Merge PR #14107: Gitignore update for doc_grammar and omega clean-up.coqbot-app[bot]
Reviewed-by: jfehrle
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]
Reviewed-by: jfehrle
2021-04-10Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on ↵coqbot-app[bot]
red/orange background) Reviewed-by: Zimmi48 Ack-by: cpitclaudel
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
Fixes #14092: Print Grammar ltac2 should exist.
2021-04-07Merge PR #14008: [stdlib] [Arith] Cantor pairingcoqbot-app[bot]
Reviewed-by: olaure01 Ack-by: jfehrle
2021-04-06Merge PR #14077: Add odoc warnings for empty packages.coqbot-app[bot]
Reviewed-by: ejgallego
2021-04-06Merge PR #13741: Remove omega tactic (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross Ack-by: silene Ack-by: SkySkimmer Ack-by: olaure01
2021-04-06Add odoc warnings for empty packages.Théo Zimmermann
From an OCaml library point of view.
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
add polynomial specifications of to_nat add changelog and doc entries
2021-04-01Merge PR #14044: [RM] changelog for 8.13.2coqbot-app[bot]
Reviewed-by: Zimmi48
2021-04-01Merge PR #14018: [doc] [coq_makefile] Document that -j N is broken for OCaml ↵coqbot-app[bot]
< 4.07.0 Reviewed-by: JasonGross Ack-by: jfehrle
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-01Update doc/sphinx/changes.rstEnrico Tassi
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-01changelog for 8.13.2Enrico Tassi
2021-03-30Properly expand projection parameters in Btermdn.Pierre-Marie Pédrot
The old code was generating different patterns, depending on whether a projection with parameters was expanded or not. In the first case, parameters were present, whereas in the latter they were not. We fix this by adding dummy parameter arguments on sight. Fixes #14009: TC search failure with primitive projections.
2021-03-30Merge PR #14012: Fix Ltac2 `Array.init` exponential overheadPierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: ppedrot
2021-03-30Merge PR #14005: Support OCaml primitives with an actual arity larger than 4.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2021-03-30Merge PR #13997: Add an Ltac1 to Ltac2 FFI for identifiers.Michael Soegtrop
Reviewed-by: MSoegtropIMC
2021-03-29[doc] [coq_makefile] Document that -j N is broken for OCaml < 4.07.0Emilio Jesus Gallego Arias
Fixes #10704
2021-03-29Merge PR #13986: [stdlib] [List] removed deprecated/unnecessary ↵coqbot-app[bot]
dependencies: Le, Gt, Minus, Lt, Setoid Reviewed-by: anton-trunov
2021-03-29Added a changelog.Pierre-Marie Pédrot
2021-03-26Document as critical.Guillaume Melquiond
2021-03-26Fix Ltac2 `Array.init` exponential overheadJason Gross
Previously, `Array.init` was computing the first element of the array twice, resulting in exponential overhead in the number of recursive nestings of `Array.init`. Notably, since `Array.map` is implemented in terms of `Array.init`, this exponential blowup shows up in any term traversal based on `Array.map` over the arguments of application nodes. Fixes #14011
2021-03-26Adding a changelog.Pierre-Marie Pédrot
2021-03-26remove in List.v deprecated/unnecessary dependencies: Le, Gt, Minus, Lt, SetoidAndrej Dudenhefner
fix unexpectedly broken MSetGenTree.v add changelog entry
2021-03-26Merge PR #13955: [stdlib] [List] added map and Forall / Exists lemmascoqbot-app[bot]
Reviewed-by: olaure01
2021-03-25Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths ↵coqbot-app[bot]
to check for conversion Reviewed-by: gares Ack-by: SkySkimmer
2021-03-25Merge PR #13852: [vernac] Improve alpha-renaming in record projection typescoqbot-app[bot]
Reviewed-by: SkySkimmer
2021-03-23Merge PR #13774: Allow to register deprecation status in Ltac2 term and ↵Michael Soegtrop
notation declarations Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-03-23Merge PR #13914: Allow the presence of type casts for return values in Ltac2.Michael Soegtrop
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48
2021-03-23add lemmas to List.v: Exists_map, Exists_concat, Exists_flat_map, ↵Andrej Dudenhefner
Forall_map, Forall_concat, Forall_flat_map, nth_error_map, nth_repeat, nth_error_repeat
2021-03-23Merge PR #13671: [stdlib] [Vectors] add results on to_listcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-23Merge PR #13804: [stdlib] [List] Add results about count_occcoqbot-app[bot]
Reviewed-by: anton-trunov
2021-03-16correct changelog #13582Olivier Laurent
2021-03-16add changelogOlivier Laurent
2021-03-16Adding a changelog and registering the new file in the documentation.Pierre-Marie Pédrot
2021-03-13Documenting the changes.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:14:02 +0000