aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/user-extensions
AgeCommit message (Collapse)Author
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-20Documentation of the support for general single binders in notations.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
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-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-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-05Rename Dec and HexDec to Decimal and HexadecimalPierre Roux
As noted by Hugo Herbelin, Dec is rather used for "decidable".
2020-11-05[refman] Add an example for number notationsPierre Roux
As suggested by Jim Fehrle while reviewing #12218
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05[numeral notation] Add support for parameterized inductivesPierre Roux
2020-11-05[numeral notation] Handle implicit argumentsPierre Roux
2020-11-05[numeral notation] Document the via ... using ... optionPierre Roux
2020-10-30Renaming numnotoption into number_modifierPierre Roux
2020-10-30Renaming Numeral.v into Number.vPierre Roux
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename tactic_expr -> ltac_exprJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-10Documenting the new only-parsing only-printing model.Hugo Herbelin
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-09-14Merge PR #13022: Fixing documentation relatively to example of use of extra ↵coqbot-app[bot]
spaces in notations Reviewed-by: jfehrle
2020-09-13Fixing documentation relatively to example of use of extra spaces in notations.Hugo Herbelin
2020-09-11[numeral notation] Improve documentationPierre Roux
Following reviews from Jim Fehrle on #12218 and #12979
2020-09-11Rename Numeral Notation command to Number NotationPierre Roux
Keep Numeral Notation wit a deprecation warning.
2020-09-11[refman] Explicit integer and naturalPierre Roux
As respectively bigint and bignat that fit into an OCaml int.
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename numeral to numberPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-08-03More documentation on grammars and parsingJim Fehrle
2020-07-17Documenting new primitive entry evaluable_ref usable for tactic notations.Hugo Herbelin
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-15Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into ↵Clément Pit-Claudel
multiple pages. Reviewed-by: jfehrle
2020-05-15Merge PR #11948: Hexadecimal numeralsHugo Herbelin
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: herbelin
2020-05-14Fix conflicts with latest master.Théo Zimmermann
2020-05-14Add some markers of origin.Théo Zimmermann
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-13Documenting notations with both terms and binders.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-05-09Add a `with_strategy` tacticJason Gross
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g., `Opaque foo` doesn't break some automation which tries to unfold `foo`. We have some timeouts in the strategy success file. We should not run into issues, because we are not really testing how long these take. We could just as well use `Timeout 60` or longer, we just want to make sure the file dies more quickly rather than taking over 10^100 steps. Note that this tactic does not play well with `abstract`; I have a potentially controversial change that fixes this issue. One of the lines in the doc comes from https://github.com/coq/coq/pull/12129#issuecomment-619771556 Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr> Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr> Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
2020-05-09[doc] Add hexadecimal numeralsPierre Roux
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-23Merge PR #12148: Consolidate funind documentation onto a single page.Clément Pit-Claudel
Reviewed-by: jfehrle
2020-04-20Remove Functional Scheme from Scheme chapter.Théo Zimmermann
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 01:57:24 +0000