aboutsummaryrefslogtreecommitdiff
path: root/parsing/pcoq.ml
AgeCommit message (Expand)Author
2021-04-23Relying on the abstract notion of streams with location for parsing.Hugo Herbelin
2020-12-11Revert removal of eoi_entry in #13447Jim Fehrle
2020-11-22Remove unused parsing codeJim Fehrle
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
2020-10-27Rename misc nonterminalsJim Fehrle
2020-10-27Rename operconstr -> termJim Fehrle
2020-10-14Deprecating wit_var to the benefit of its synonymous wit_hyp.Hugo Herbelin
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is de...Hugo Herbelin
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-09-11Adding a wit_natural standard argument.Hugo Herbelin
2020-09-11[parsing] Rename token NUMERAL to NUMBERPierre Roux
2020-05-09Add a `with_strategy` tacticJason Gross
2020-03-25[pcoq] Inline the exported Gramlib interface instead of exposing it as GEmilio Jesus Gallego Arias
2020-03-25[gramlib] Remove warning function parameter in favor of standard mechanism.Emilio Jesus Gallego Arias
2020-03-25[parsing] Move `coq_parsable` custom logic to Grammar.Emilio Jesus Gallego Arias
2020-03-25[parsing] Remove redundant interfaces from PcoqEmilio Jesus Gallego Arias
2020-03-25[parsing] Remove unneeded `Extend.entry` type.Emilio Jesus Gallego Arias
2020-03-25[parsing] Remove extend AST in favor of gramlib constructorsEmilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar rules private.Emilio Jesus Gallego Arias
2020-03-25[parsing] Make grammar extension type private.Emilio Jesus Gallego Arias
2020-03-22Centralizing all kinds of numeral string management in numTok.ml.Hugo Herbelin
2020-03-22Adding bignat to parse positive numbers; bigint now includes negative ints.Hugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-08Merge PR #11714: [gramlib] Refactor gramlib interface.Pierre-Marie Pédrot
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
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
2020-02-28[gramlib] Refactor gramlib interface.Emilio Jesus Gallego Arias
2020-02-21[parsing] Track need to reinit by typingEmilio Jesus Gallego Arias
2019-12-22Ensure that a custom entry cannot be defined twice.Pierre-Marie Pédrot
2019-11-19Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.Hugo Herbelin
2019-10-13Doc update with mlg extension - fix #10855mcaci
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-06-19Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations i...Théo Zimmermann
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-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-23Fixing typos - Part 2JPR
2019-03-31Multiple payload types in tokensPierre Roux
2019-03-31[parsing] Split Tok.t into Tok.t and Tok.patternEnrico Tassi
2019-03-29[parser] initialization based on Loc.t rather than Loc.sourceEnrico Tassi
2019-01-24[STM] explicit handling of parsing statesEnrico Tassi
2018-12-13Move shallow state logic to the function preparing state for workersMaxime Dénès
2018-11-30[gramlib] Remove `Ploc.t` in favor of `Loc.t`Emilio Jesus Gallego Arias
2018-11-27[gramlib] Remove unused function `gram_reinit`.Emilio Jesus Gallego Arias
2018-11-27[pcoq] Remove a redundant `entry` type.Emilio Jesus Gallego Arias
2018-11-27[gramlib] Minor cleanups:Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:02 +0000