aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-07-01UIP in SPropGaëtan Gilbert
2020-07-01Merge PR #12596: Credit Erik Martin-Dorel for work on Docker.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-26Mention VSCoq with respect to _CoqProjectCarl Patenaude-Poulin
2020-06-26Credit Erik Martin-Dorel for work on Docker.Théo Zimmermann
2020-06-23Merge PR #12552: Add a pre-hook mechanism for the `zify` tacticFrédéric Besson
Reviewed-by: fajb
2020-06-21Add index for coqdoc.Théo Zimmermann
Fixes #12545.
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
Hope this is enough, also looking at https://github.com/coq/coq/commit/4c9ba141f8f7e067f274cb5a02293e8e52f89487#diff-a907eea979c6d310cb6208180b556d6d.
2020-06-14Update zify documentationFrédéric Besson
Add Zify <X> are documented. Add <X> is deprecated as it clashed with the standard Add command
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
2020-06-11Merge PR #12481: Minor improvements to the sections on basics and sorts.Emilio Jesus Gallego Arias
Reviewed-by: jfehrle
2020-06-10Update changelog for 8.12+beta1.Théo Zimmermann
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-09Merge PR #12103: Convert Ltac chapter to prodnThéo Zimmermann
2020-06-09Summary of changes for 8.12Matthieu Sozeau
Includes fixes to changes by Jim, Enrico and Théo Fix local links, for 8.12 and 8.11
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-06-08Make automatic name generation for directives more consistent:Jim Fehrle
- by default, generate names for all directives using the prefix "[a-zA-Z0-9_ ]+" except - don't generate a name for cmdv and tacv - generate more flexibily for exn, warn and attr
2020-06-06Merge PR #12380: Fix #12361 (indexing issues in the PDF)Théo Zimmermann
Ack-by: Zimmi48 Reviewed-by: jfehrle
2020-06-05Merge PR #12450: Document known issue of Proof <term> with PG.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: erikmd Reviewed-by: jfehrle
2020-06-05Merge PR #12460: Add remaining 8.12+beta1 changelog entries.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-05Merge PR #12459: Document incompatibility with Sphinx 3.Emilio Jesus Gallego Arias
Reviewed-by: cpitclaudel
2020-06-05Merge PR #12397: Fix #12280: do not use xindy to avoid build failures on ↵Emilio Jesus Gallego Arias
some machines. Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2020-06-05Adjust list of versions in version switcher.Théo Zimmermann
- Use the name 'dev' instead of 'master' because it is less cryptic. - Add the 'v8.12' branch. - Use the branch version only for active branches, and the latest patch-level release for the rest.
2020-06-05Add remaining 8.12+beta1 changelog entries.Théo Zimmermann
2020-06-05Document incompatibility with Sphinx 3.Théo Zimmermann
Cf. #12332
2020-06-05Fix version switcher when building with Dune.Théo Zimmermann
Closes #12395.
2020-06-05[sphinx] Get rid of anonymous targets (Sphinx 2.3.1 doesn't like them)Clément Pit-Claudel
https://github.com/sphinx-doc/sphinx/issues/7701
2020-06-04Tweak wording.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-06-04Document known issue of Proof <term> with PG.Théo Zimmermann
See #12444.
2020-06-01Merge PR #12396: Release notes 8.12Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: jfehrle
2020-05-27Promoting COQLIBINSTALL and COQDOCINSTALL in coq_makefile to the parameters ↵Martin Bodin
section.
2020-05-27Add more changelog entries which have been backported to v8.12.Théo Zimmermann
2020-05-27[changelog/8.12] Wording improvements.Théo Zimmermann
2020-05-27[changelog/8.12] Use sections and provide a local TOC.Théo Zimmermann
2020-05-27[changelog/8.12] Split misc entries out in more relevant sections.Théo Zimmermann
2020-05-27Changelog entries for the 8.12 changes to the reference manual.Théo Zimmermann
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-26Fix #12280: do not use xindy to avoid build failures on some machines.Théo Zimmermann
2020-05-24Fix hyperlinks in changes.rstMatthew Dempsky
2020-05-22Merge PR #11986: [primitive floats] Add low level printingPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-05-19[primitive floats] Add low level hexadecimal printingPierre Roux
2020-05-18Use the new gdef alt-text feature in the refman.Théo Zimmermann
2020-05-18Support :gdef:`text <term>` syntax (adding "<term>")Jim Fehrle
2020-05-18Bump minimal versions of refman dependencies.Théo Zimmermann
Fixes #11936. Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-05-16Merge PR #12326: Fix #11761: Functional Induction throws unrecoverable error.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-05-16Merge PR #12330: Add redirects for HTML pages that were moved.Clément Pit-Claudel
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: kyoDralliam
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 10:08:22 +0000