aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
2020-11-28Merge PR #13496: Revert "Remove deprecated tactic cutrewrite."coqbot-app[bot]
Reviewed-by: gares
2020-11-27Merge PR #12586: [declare] Allow custom typing flags when declaring constants.coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: herbelin Ack-by: jfehrle
2020-11-27Merge PR #13483: Fix #13283: improved error on `clear implicit` flagcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
2020-11-27Improved error message on nested proofsFabian Kunze
to include most common reason when this happens on accident
2020-11-27Fix #13283: improved error on `clear implicit` flagFabian Kunze
2020-11-26[attributes] [typing] Rename `typing` to `bypass_check`Emilio Jesus Gallego Arias
As discussed in the Coq meeting.
2020-11-26[attributes] [doc] Documentation review by Théo.Emilio Jesus Gallego Arias
Co-authored-by: <Théo Zimmermann <theo.zimmermann@inria.fr>
2020-11-26[vernac] Allow to control typing flags with attributes.Emilio Jesus Gallego Arias
The syntax is the one of boolean attributes, that is to say `#[typing($flag={yes,no}]` where `$flag` is one of `guarded`, `universes`, `positive`. We had to instrument the pretyper in a few places, it is interesting that it is doing so many checks.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 08:30:32 +0000