aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/orderedGrammar
AgeCommit message (Expand)Author
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
2021-04-12Remove omega from doc_grammar files.Théo Zimmermann
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-03-30Remove the :> type castJim Fehrle
2021-03-10Regenerate the Ltac2 syntax for documentation.Pierre-Marie Pédrot
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-01-28Replace : term with : type in open binders.Théo Zimmermann
2021-01-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` into...Pierre-Marie Pédrot
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
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notat...coqbot-app[bot]
2020-11-22Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".Hugo Herbelin
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]
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]
2020-11-16Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"coqbot-app[bot]
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 d...coqbot-app[bot]
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]
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
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
2020-09-11[refman] Explicit integer and naturalPierre Roux
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:34:42 +0000