aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Collapse)Author
2020-03-03When parsing negative integer, ensure minus sign is contiguous to the number.Hugo Herbelin
For instance, formerly, "Set Inline Level - 1" was succeeding. Now only "Set Inline Level -1" succeeds. (Even though -1 does not make sense for a Inline Level, but that's then a semantic issue. Other options may accept negative numbers in general.)
2020-03-01[parser] lk_int -> lk_natMaxime Dénès
2020-03-01Refactor lookaheads using DSLMaxime Dénès
2020-03-01Move lookahead combinators to PcoqMaxime Dénès
They were in Ltac2, but they are of general interest
2020-02-28[gramlib] Refactor gramlib interface.Emilio Jesus Gallego Arias
This is in preparation for making the Gramlib interface the canonical one; see #11647 . I tried to implement some of the ideas that were floated around in a chat with Pierre-Marie, suggestions / comments are welcome.
2020-02-27Merge PR #11650: Set Printing ParensEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-02-25Merge PR #11655: [parsing] Track need to reinit by typingPierre-Marie Pédrot
Reviewed-by: ppedrot
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-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-21[parsing] Track need to reinit by typingEmilio Jesus Gallego Arias
This PR is in preparation of #9067 (together with #11647) . Before this PR, `grammar_extend` always took an optional `reinit` argument, even if it was never set to `Some ...`. Indeed, there is a single case where reinit is needed; we track it now by using a different extension rule constructor.
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-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-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-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
2019-12-22Ensure that a custom entry cannot be defined twice.Pierre-Marie Pédrot
This highlights the fact that diamond inheritance of a custom entry is a tricky problem, as well as merely importing two custom entries with the same name from two different modules. The only sane way to give a semantics to that is to stick to module-scoped objects, i.e. give those entries a kernel name. In the meantime, I went for a warning when overriding entries.
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès
Fixes #9532 Fixes #9490
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ```
2019-11-19G_constr: Renaming record_fields_instance -> fields_def.Hugo Herbelin
This is in accordance with PR #10614 and to avoid a confusion with the fields of a record type in g_vernac.ml. Removing a useless line at the same time in G_vernac.
2019-11-19G_constr: Renaming instance -> univ_instance (more specific name).Hugo Herbelin
2019-11-19G_constr: Uniformization of indentation.Hugo Herbelin
2019-11-19Separating constr grammar for fix and cofix, for the purpose of documentation.Hugo Herbelin
2019-11-19Grammar: slight simplification of treatment of annot/binder overlapping.Hugo Herbelin
2019-11-19Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.Hugo Herbelin
2019-11-19Grammar of terms: mini-shortcut in the rules for fix and cofix.Hugo Herbelin
2019-11-15Merge PR #11079: Rename non-unique local nonterminalsHugo Herbelin
Ack-by: Zimmi48 Ack-by: herbelin
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-11Miscellaneous improvements of the syntax of records.Hugo Herbelin
- only one space instead of two when printing "{| |}" - removing a redundant clause in the grammar of record_patterns
2019-10-30Rename the 2 local type_cstr nonterminals to give them unique namesJim Fehrle
2019-10-25Possible simplification of parsing rules.Théo Zimmermann
Noticed by Jim while working on automatic grammar documentation.
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
Ack-by: ejgallego Reviewed-by: gares
2019-08-29Merge PR #9066: [parsing] Move pcoq-specific parts in extend to pcoq.Pierre-Marie Pédrot
Reviewed-by: ppedrot
2019-08-29Fix a few wrong uses of `msg_notice`Maxime Dénès
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
This improves error reporting. Addendum to #10515
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
We move `binder_kind` to the pretyping AST, removing the last data type in the now orphaned file `Decl_kinds`. This seems a better fit, as this data is not relevant to the lower layers but only used in `Impargs`. We also move state keeping to `Impargs`, so now implicit declaration must include the type. We also remove a duplicated function.
2019-08-19[pcoq] Remove unneeded casting operators.Emilio Jesus Gallego Arias
2019-08-19[parsing] Move pcoq-specific parts in extend to pcoq.Emilio Jesus Gallego Arias
2019-08-06[parsing] unify checks for contiguity of tokens in Ltac2 and G_primEnrico Tassi
2019-08-02[lexer]: improve error message on loct_func misuseEnrico Tassi
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-06-24Merge PR #10375: [lexer] correctly update line number when lexing QUOTATION ↵Pierre-Marie Pédrot
(fix #10350) Ack-by: gares Reviewed-by: ppedrot
2019-06-19Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations ↵Théo Zimmermann
in favor of "simple_intropattern" Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-06-18[lexer] correctly update line number when lexing QUOTATION (fix #10350)Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:16:58 +0000