aboutsummaryrefslogtreecommitdiff
path: root/parsing/pcoq.ml
AgeCommit message (Expand)Author
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
2018-11-23Remove the unsafe camlp5 API from the Coq codebase.Pierre-Marie Pédrot
2018-11-23Port Pcoq to safe camlp5 API.Pierre-Marie Pédrot
2018-11-21[gramlib] [build] Switch make-based system to packed gramlibEmilio Jesus Gallego Arias
2018-11-19[gramlib] Remove unused alias.Emilio Jesus Gallego Arias
2018-11-08Revert "Merge PR #8923: Bump camlp5 minimal version and use its safe API."Pierre-Marie Pédrot
2018-11-07Port to safe camlp5 API.Pierre-Marie Pédrot
2018-07-29Store marshallable data in the custom entry summary.Pierre-Marie Pédrot
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
2018-07-29Adding support for custom entries in notations.Hugo Herbelin
2018-07-29Synchronizing "grammars by name" with backtrack (custom entries shall be adde...Hugo Herbelin
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 23:03:30 +0000