aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/orderedGrammar
AgeCommit message (Collapse)Author
2021-01-28Replace : term with : type in open binders.Théo Zimmermann
And update the doc_grammar files.
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` ↵Pierre-Marie Pédrot
into `pat:` Ack-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: ppedrot
2021-01-13Adjust the doc_grammar files.Théo Zimmermann
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
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-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-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-18Run doc_grammar for #13312.Théo Zimmermann
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-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Update grammar in docJim Fehrle
2020-11-15Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"Jim Fehrle
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-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-14Move destructuring let syntax closer to its documentation.Théo Zimmermann
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-09Add global version of OPTINREFJim Fehrle
2020-11-05Merge PR #12218: Numeral notations for non inductive typescoqbot-app[bot]
Reviewed-by: herbelin Reviewed-by: JasonGross Reviewed-by: jfehrle Ack-by: Zimmi48
2020-11-05[string notation] Handle parameterized inductives and non inductivesPierre Roux
2020-11-05[numeral notation] Handle implicit argumentsPierre Roux
2020-11-05[numeral notation] Document the via ... using ... optionPierre Roux
2020-11-04[numeral notation] Adding the via ... using ... optionPierre Roux
This enables numeral notations for non inductive types by pre/postprocessing them to a given proxy inductive type. For instance, this should enable the use of numeral notations for R.
2020-11-04Regenerate the grammar description file.Pierre-Marie Pédrot
2020-10-30Renaming numnotoption into number_modifierPierre Roux
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-12Add missing ";" in record grammarJim Fehrle
2020-10-05Document the removal of forward class hints.Théo Zimmermann
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-11Adding a wit_natural standard argument.Hugo Herbelin
2020-09-11Turn integer into natural in several mlgsPierre Roux
Negative values had no meaning there. Those were spotted by Hugo Herbelin while reviewing #12979 .
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-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-15Document new Search features.Théo Zimmermann
2020-05-15Update docgram following #12122 and #12229.Théo Zimmermann
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-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-13Update syntax of Import / Export in documentation.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-01 19:24:39 +0000