aboutsummaryrefslogtreecommitdiff
path: root/parsing/g_constr.mlg
AgeCommit message (Expand)Author
2021-03-30Remove the :> type castJim Fehrle
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-20A step towards supporting pattern cast deeplier.Hugo Herbelin
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
2020-10-30Renaming Numeral into NumberPierre Roux
2020-10-27Change a few nonterminal names in mlgs and update doc to matchJim Fehrle
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is de...Hugo Herbelin
2020-10-10Add location in existential variable names (CEvar/GEvar).Hugo Herbelin
2020-10-10Adding and using locations on identifiers in constr_expr where they were miss...Hugo Herbelin
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-07-06Primitive persistent arraysMaxime Dénès
2020-07-03Fix #11121: Simultaneous definition of term and notation in custom grammarMaxime Dénès
2020-05-06Stop keeping outdated static list of keywords.Hugo Herbelin
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-01Refactor lookaheads using DSLMaxime Dénès
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-04Add syntax for non maximally inserted implicit argumentsSimonBoulier
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-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-06-17Update ml-style headers to new year.Théo Zimmermann
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-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
2019-04-02Rename the INT token to NUMERALPierre Roux
2019-04-01Replace type sign = bool with SPlus | SMinusPierre Roux
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2018-11-23Remove the unsafe camlp5 API from the Coq codebase.Pierre-Marie Pédrot
2018-10-05Using smart mkLambdaCN/mkProdCN.Hugo Herbelin
2018-09-02Fixing #7867 (class error message tries to print a "fun" with no binder).Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-06-29Port g_constr to the homebrew GEXTEND parser.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:35 +0000