aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2020-02-22Merge PR #11635: Cleanup around the tolerability structureEmilio Jesus Gallego Arias
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
2020-02-21Notations: Avoiding computing parsing rule when in onlyprinting mode.Hugo Herbelin
2020-02-20Merge PR #10832: Addressing #6082 and #7766: warning when overriding notation...Emilio Jesus Gallego Arias
2020-02-19Revert "Granting #9516 and #9518 (support for numerals and strings in custom ...Hugo Herbelin
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-16Revert "Suite picking numeral notation"Hugo Herbelin
2020-02-16Suite picking numeral notationHugo Herbelin
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
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
2019-12-20Fix handling of recursive notations with custom entriesMaxime Dénès
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-19G_constr: Renaming record_fields_instance -> fields_def.Hugo Herbelin
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
2019-11-14Rename non-unique local nonterminalsJim Fehrle
2019-11-11Miscellaneous improvements of the syntax of records.Hugo Herbelin
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
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-08-29Merge PR #9066: [parsing] Move pcoq-specific parts in extend to pcoq.Pierre-Marie Pédrot
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
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
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
2019-06-19Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations i...Théo Zimmermann
2019-06-18[lexer] correctly update line number when lexing QUOTATION (fix #10350)Enrico Tassi
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-16Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".Hugo Herbelin
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-06-01Towards unifying parsing/printing for universe instances and Type's argument.Hugo Herbelin
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-23Fixing typos - Part 2JPR
2019-05-16binder_kind Generalized: remove 1st arg as it's always ImplicitGaëtan Gilbert
2019-04-16[ast] [constrexpr] Make recursion_order_expr an AST node.Emilio Jesus Gallego Arias
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 04:45:37 +0000