aboutsummaryrefslogtreecommitdiff
path: root/vernac/metasyntax.ml
AgeCommit message (Collapse)Author
2021-04-07[abbreviation] allow the user to set arguments scopeEnrico Tassi
2021-04-07cleanup: less exceptions, removal of try_interp_name_aliasEnrico Tassi
2021-04-06Missing dot in an error message.Hugo Herbelin
2021-04-06Uniformizing the "already exists" messagesHugo Herbelin
2021-01-04Remember universe instances of constants in notationsJasper Hugunin
2020-12-06Fix spelling in warning entrySimon Friis Vindum
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
We use a deprecation phase where: - "ident" means "name" (as it used to mean), except in custom coercion entries where it already meant "ident". - "ident" will be made again available (outside situation of coercions) to mean "ident" at the end of deprecation phase. Also renaming "as ident" into "as name". Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
We introduce a class of open binders which includes "x", "x:t", "'pat" and a class of closed binders which includes "x", "(x:t)", "'pat".
2020-11-15Moving the analysis of notation strings in notation.ml.Hugo Herbelin
This is a better abstraction barrier (no "symbol" type with uninterpreted ".." exported out of notation.ml). It also allows to "browse" notations mentioning a "..".
2020-11-03Merge PR #13092: Fixing #13078: stack overflow and anomalies with binding ↵coqbot-app[bot]
notations in patterns Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: LasseBlaauwbroek
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-19Addressing parsing part #13078.Hugo Herbelin
We don't give sense to pattern/binders in leftmost position.
2020-10-19Fixing printing part of #13078 (anomaly with binding notations in patterns).Hugo Herbelin
We prevent notations involving binders (i.e. names or patterns) to be used for printing in "match" patterns. The computation is done in "has_no_binders_type", controlling uninterpretation.
2020-10-10Adding a warning in case a notation is used neither for parsing nor printing.Hugo Herbelin
2020-10-10Notations: reworking the treatment of only-parsing and only-printing notations.Hugo Herbelin
The (old) original model for notations was to associated both a parsing and a printing rule to a notation. Progressively, it become more and more common to have only parsing notations or even multiple expressions printed with the same notation. The new model is to attach to a given scope, string and entry at most one either only-parsing or mixed-parsing-printing rules + an arbitrarily many unrelated only-printing rules. Additionally, we anticipate the ability to selectively activate/deactivate each of those. This allows to fix in particular #9682 but also to have more-to-the-point warnings in case a notation overrides or partially overrides another one. Rules for importing are not changed (see forthcoming #12984 though). We also improve the output of "Print Scopes" so that it adds when a notation is only-parsing, only-printing, or deactivated, or a combination of those. Fixes #4738 Fixes #9682 Fixes part 2 of #12908 Fixes #13112
2020-10-08Merge PR #12949: When a notation is only parsing, do not attach to it a ↵coqbot-app[bot]
specific format. Reviewed-by: ejgallego
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-15A temporary fix of #13018 and #12775 for branch 8.2.Hugo Herbelin
We arbitrarily use max_int as higher level of custom entries in printing, which should be ok since only < and <= are used to decide when to use coercions.
2020-09-10When a notation is only parsing, do not attach to it a specific format.Hugo Herbelin
2020-08-25Moving production_level_eq to extend.ml for separation of concerns.Hugo Herbelin
Add a mli file and uniformize indentation on the way.
2020-08-25A fix and two enhancements of trailing pattern factorization in rec. notations.Hugo Herbelin
The fix is a missing check of equality of custom entries. The enhancements are: - not to bother breaking hints - not to care about the border or internal position when the level is made explicit Ideally, one could also improve the treatment of DefaultLevel. To be done later on.
2020-07-15Fix bug #12691 (an only parsing notation induces a generic printing format).Hugo Herbelin
This is to anticipate further not-only-parsing uses of the notation.
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-05-14Merge PR #11922: No more local reduction functions in Reductionops.Maxime Dénès
Reviewed-by: Matafou Ack-by: SkySkimmer Reviewed-by: gares
2020-05-13Extending support for mixing binders and terms in abbreviations.Hugo Herbelin
2020-05-10No more local reduction functions in Reductionops.Pierre-Marie Pédrot
This is extracted from #9710, where we need the environment anyway to compute iota rules on inductive types with let-bindings. The commit is self-contained, so I think it could go directly in to save me a few rebases. Furthermore, this is also related to #11707. Assuming we split cbn from the other reduction machine, this allows to merge the "local" machine with the general one, since after this PR they will have the same type. One less reduction machine should make people happy.
2020-04-13pass filters aroundGaëtan Gilbert
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
Four types of numerals are introduced: - positive natural numbers (may include "_", e.g. to separate thousands, and leading 0) - integer numbers (may start with a minus sign) - positive numbers with mantisse and signed exponent - signed numbers with mantisse and signed exponent In passing, we clarify that the lexer parses only positive numerals, but the numeral interpreters may accept signed numerals. Several improvements and fixes come from Pierre Roux. See https://github.com/coq/coq/pull/11703 for details. Thanks to him.
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-09Fix #11730: Mangle Names vs InfixGaëtan Gilbert
2020-03-04Experimenting using a record for decl_notation.Hugo Herbelin
2020-03-04Adding support for an "only parsing" modifier in "where"-based notations.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
We make the primitives for backtrace-enriched exceptions canonical in the `Exninfo` module, deprecating all other aliases. At some point dependencies between `CErrors` and `Exninfo` were a bit complex, after recent clean-ups the roles seem much clearer so we can have a single place for `iraise` and `capture`.
2020-02-23Cancelling precedences in Set Printing Parentheses only at border of notations.Hugo Herbelin
2020-02-22Merge PR #11635: Cleanup around the tolerability structureEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-22Fixing a bug introduced in PR #10832 (new format specific to a given notation).Hugo Herbelin
The import of the format should not be done if i<>1 in open_notation.
2020-02-22Simplification of type unparsing (index of variable in UnpMetaVar is unused).Hugo Herbelin
2020-02-22Making structure of type "tolerability" and related clearer.Hugo Herbelin
Also renamed it to relative_entry_level. Correspondence between old and new representation is: (n,L) -> LevelLt n (n,E), (n,Prec n) -> LevelLe n (n,Any) -> LevelSome (n,Prec p) when n<>p was unused Should not change global semantics (except error message in pr_arg).
2020-02-22Preparing to simplifying the structure of type "tolerability".Hugo Herbelin
The "Any" case was not reached formerly for ETPattern and ETConstr as far as I can see. So there should be no change of semantics.
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
In particular, this fixes #9741.
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding ↵Emilio Jesus Gallego Arias
notation format + new notion of format associated to a given interpretation Ack-by: maximedenes
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ↵Hugo Herbelin
entries)." This reverts commit 29919b725262dca76708192bde65ce82860747be. It was pushed by mistake as part of #11530. Sorry about it.
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
We do two changes: - We distinguish between a notion of format generically attached to notations and a new notion of format attached to interpreted notations. "Reserved Notation" attaches a format generically. "Notation" attaches the format specifically to the given interpretation, and additionally, attaches it generically if it is the first time the notation is defined. - We warn before overriding an explicitly reserved generic format, or a specific format.
2020-02-19Only parsing in Reserved Notation: turning notice into a warning.Hugo Herbelin
2020-02-16Revert "Suite picking numeral notation"Hugo Herbelin
This reverts commit 03c48bb6943312e606b80b7af65b1ccb7122a386.
2020-02-16Suite picking numeral notationHugo Herbelin
Ceci est une suite à numeral notation in custom entries, cherchant à raffiner la compatibilité entre entrées. C'est mélangé avec le "pick" précédent, et c'est en chantier.
2020-02-16Granting #9516 and #9518 (support for numerals and strings in custom entries).Hugo Herbelin
2020-02-16Custom entries: accept that no level is mentioned for a subentry.Hugo Herbelin
If it is for an internal non-terminal then: - if for a subentry different from constr, it refers to the head of the subentry - if in constr, it is 200 by convention If it is on the border of a rule, then: - if it is in a subentry different from the entry it lives, it refers to the head of the subentry (or 200 by convention if in constr) - if it is in the same entry, the rule for associativity tells if a SELF, a NEXT, or (if on the right) a LEVEL
2020-02-15Reorganize type "production_level" along a more intuitive structure.Hugo Herbelin
NextLevel = at next level NumLevel n = at level n DefaultLevel = <no mention of level>
2020-02-15Fixing a precedence printing bug with custom entries.Hugo Herbelin
Insertion of coercion to manage precedence of custom entries are treated in constrextern.ml, while ppconstr.ml is only about the management of precedences for constr.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:17:09 +0000