aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term ↵coqbot-app[bot]
notations. Reviewed-by: jfehrle Reviewed-by: gares Reviewed-by: Zimmi48 Reviewed-by: maximedenes
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make ↵coqbot-app[bot]
sense Reviewed-by: Zimmi48
2020-11-22Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".Hugo Herbelin
For constr, this means clarifying that "ident" is deprecated and to be replaced by "name". Here, some cleaning shall have to be done at the end of deprecation phase, when "ident" will take its literal meaning. For custom notations, this is about documenting the effect of "ident" and "global" which was yet undocumented. Note that we anticipate an example in constr working with the literal meaning of "ident" (temporarily silencing the warning). Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the ↵Pierre-Marie Pédrot
same time (granting #9816) Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-20Documentation of the support for general single binders in notations.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2020-11-19Fix typo in rst link syntax.Théo Zimmermann
2020-11-19Merge PR #12984: [printing] Order notations by matching precision first, and ↵coqbot-app[bot]
then by last imported Reviewed-by: Zimmi48 Ack-by: RalfJung Ack-by: gares
2020-11-18Merge PR #13312: [attributes] Allow boolean, single-value attributes.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: SkySkimmer Ack-by: gares
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-18[attributes] Update error message referring to deprecated syntax.Emilio Jesus Gallego Arias
2020-11-18Review commit: improving the doc of boolean attributes.Théo Zimmermann
2020-11-18Run doc_grammar for #13312.Théo Zimmermann
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog.
2020-11-18Merge PR #13400: [doc] add a link to v8.13coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-18Merge PR #13220: Give a typical example of Makefile wrapper for coq_makefile ↵coqbot-app[bot]
(addresses #12903) Reviewed-by: gares Ack-by: Zimmi48 Ack-by: SkySkimmer
2020-11-18Update doc/sphinx/practical-tools/utilities.rstHugo Herbelin
Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
2020-11-18Ref. man.: showing the x ⪯ y ⪯ .. ⪯ z ⪯ t example of recursive notation.Hugo Herbelin
2020-11-17Documenting priority given to most recently declared/imported notations.Hugo Herbelin
2020-11-17Documenting the preference given to more precise notations at printing time.Hugo Herbelin
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot
2020-11-17Fixes #13235: remove fragile tolerance for degenerate in-hyps clause.Hugo Herbelin
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-16[doc] add a link to v8.13Enrico Tassi
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Merge PR #12516: Deprecate `Grab Existential Variables` and `Existential` ↵Pierre-Marie Pédrot
commands Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: ppedrot
2020-11-16Document the deprecation of the commands.Pierre-Marie Pédrot
2020-11-16Document the new warning.Pierre-Marie Pédrot
2020-11-16Tentative fix for the refman.Pierre-Marie Pédrot
2020-11-16Merge PR #13388: Export locality for all hint commandscoqbot-app[bot]
Reviewed-by: silene Reviewed-by: gares Reviewed-by: Zimmi48
2020-11-16Update grammar in docJim Fehrle
2020-11-16Doc for variance syntaxGaëtan Gilbert
2020-11-15Merge PR #13308: Address #13304: in coqdoc, clearly distinguish block ↵Li-yao Xia
verbatim from inline verbatim Reviewed-by: Lysxia
2020-11-15Merge PR #13375: Distinguish one_pattern and one_term nonterminals, improve ↵coqbot-app[bot]
description of Instance command Reviewed-by: Zimmi48
2020-11-15Document the new export locality for the remaining hint commands.Pierre-Marie Pédrot
2020-11-15Doc and changelog for Instance Generalized OutputGaëtan Gilbert
2020-11-14Documenting one-line verbatim.Hugo Herbelin
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-14Move destructuring let syntax closer to its documentation.Théo Zimmermann
2020-11-12Move last changelog entry for 8.12.1.Théo Zimmermann
2020-11-12Merge PR #13331: Fix #13330: Kernel messes with polymorphic side-effects.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: SkySkimmer Ack-by: gares Ack-by: jfehrle Ack-by: jashug Ack-by: ejgallego
2020-11-12Merge PR #13345: Addressing #13344: clarifying the role of Add ML Path vs -Icoqbot-app[bot]
Reviewed-by: ejgallego Reviewed-by: Zimmi48 Ack-by: ppedrot Ack-by: jfehrle
2020-11-12Add documentation about the soundness bug.Pierre-Marie Pédrot
2020-11-12Clarifying the role of Add ML Path vs -I (see #13344).Hugo Herbelin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-12Merge PR #13317: [ssr] intro pattern extensions for dup, swap and applycoqbot-app[bot]
Reviewed-by: gares Ack-by: Zimmi48
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 07:20:16 +0000