aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2020-08-19Fixes #10902 by adding a mention of the JSON extraction in the documentation.Martin Bodin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-08-17Merge PR #12841: Recommend replace as a replacement to cutrewrite.coqbot
Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-08-17Merge PR #12802: Document semantic restriction on patterns in Gallina match ↵coqbot
construct Reviewed-by: Zimmi48 Ack-by: gares Ack-by: jfehrle
2020-08-17Recommend replace as a replacement to cutrewrite.Théo Zimmermann
As suggested by Laurent Thery to Chris Dams on Coq-Club. (And fix the documented syntax in the manual.)
2020-08-15Document semantic restriction on patternsJim Fehrle
2020-08-13Merge PR #12556: Bring Float notations in line with stdlibHugo Herbelin
Reviewed-by: erikmd Reviewed-by: herbelin
2020-08-11Merge PR #12717: More documentation on grammars and parsingPierre-Marie Pédrot
Reviewed-by: Zimmi48 Ack-by: herbelin Reviewed-by: ppedrot
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
Reviewed-by: CohenCyril Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-09Bring Float notations in line with stdlibJason Gross
This is a companion to #12479 as per https://github.com/coq/coq/pull/12479#issuecomment-641336039 that changes some of the PrimFloat notations: - `m == n` into `m =? n` to correspond with the eqb notations elsewhere - `m < n` into `m <? n` to correspond with the ltb notations elsewhere - `m <= n` into `m <=? n` to correspond with the leb notations elsewhere We also put them in a module, so users can `Require PrimFloat. Import PrimFloat.PrimFloatNotations` without needing to unqualify the primitives. Fixes the part of #12454 about floats
2020-08-07Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM ↵coqbot
environment variable Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-08-06Trying to rephrase complex sentences to make them easier to read.Martin Bodin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-08-04Document "Print Debug GC" command and OCAMLRUNPARAM env variableJim Fehrle
2020-08-03More documentation on grammars and parsingJim Fehrle
2020-07-29Fix do in ssreflect-proof-language.rstYusuke Matsushita
The tactics do in SSReflect uses `? @mult` rather than `? @num`.
2020-07-23[changelog] Incorporate hanging changelog entry for 8.12+beta1Emilio Jesus Gallego Arias
2020-07-23[changelog] Latest changes backported to 8.12 branch.Emilio Jesus Gallego Arias
2020-07-17Documenting new primitive entry evaluable_ref usable for tactic notations.Hugo Herbelin
2020-07-17Wording improvements.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-07-13Advertise switch to maintainer teams and credit maintainers.Théo Zimmermann
2020-07-11tactics.rst: `Require A` is enough for `A`'s hintsPaolo G. Giarrusso
As the text says later: > Hints should only be made available when the module they are defined in is imported, not just required.
2020-07-08Add tags in prodn indicating productions that are from plugins,Jim Fehrle
filtered-only show Ltac2 tags outside of ltac2.rst
2020-07-06Primitive persistent arraysMaxime Dénès
Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 17:11:30 +0000