aboutsummaryrefslogtreecommitdiff
path: root/doc/tools/docgram/common.edit_mlg
AgeCommit message (Collapse)Author
2021-04-23Merge PR #13965: [abbreviation] user syntax to set interp scope of argumentPierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: herbelin Reviewed-by: jashug Reviewed-by: jfehrle Reviewed-by: ppedrot
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
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-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-18Use only nats for occs_nums rather than intsJim 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] 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 tac2type -> ltac2_type,Jim Fehrle
typ_param -> ltac2_typevar, tac2expr -> ltac2_expr
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-12Add missing ";" in record grammarJim Fehrle
2020-10-05Document the removal of forward class hints.Théo Zimmermann
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-11[parsing] Simplify bigintPierre Roux
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-07-08Make local nonterminal definitions unique when necessaryJim 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-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: cpitclaudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:39:57 +0000