aboutsummaryrefslogtreecommitdiff
path: root/parsing
AgeCommit message (Expand)Author
2018-07-29Supporting locality flag for custom entries + compatibility with modules.Hugo Herbelin
2018-07-29Renaming ETName and ETReference so as to fit the user-visible terminology.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-11Merge PR #8021: Get rid of horrendous hack limiting the size of parsed integersPierre-Marie Pédrot
2018-07-08Get rid of horrendous hack limiting the size of parsed integersMaxime Dénès
2018-07-07Introduce a Pcoq.Entry module for functions that ought to be exported.Pierre-Marie Pédrot
2018-07-07Remove dead code that used to be there for CamlpX compatibility.Pierre-Marie Pédrot
2018-07-06Fix compilation of Coq with camlp5 master branch.Pierre-Marie Pédrot
2018-06-29Port g_constr to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Port g_prim to the homebrew GEXTEND parser.Pierre-Marie Pédrot
2018-06-29Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Pierre-Marie Pédrot
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-03Statment -> StatementHugo Herbelin
2018-05-31[notations] Split interpretation and parsing of notationsEmilio Jesus Gallego Arias
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-27[api] [parsing] Move Egram* to `vernac/`Emilio Jesus Gallego Arias
2018-05-23[api] Move `Vernacexpr` to parsing.Emilio Jesus Gallego Arias
2018-05-23[api] Move `opacity_flag` to `Proof_global`.Emilio Jesus Gallego Arias
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-05-04Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Pierre-Marie Pédrot
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-26[api] Move `hint_info_expr` to `Typeclasses`.Emilio Jesus Gallego Arias
2018-04-06[api] Remove dependency of library on Vernacexpr.Emilio Jesus Gallego Arias
2018-04-05Merge PR #7016: Make parsing independent of the cumulativity flag.Enrico Tassi
2018-04-04Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Enrico Tassi
2018-04-01[stm] Move VernacBacktrack to the toplevel.Emilio Jesus Gallego Arias
2018-03-30Remove deprecated commands Arguments Scope and Implicit ArgumentsJasper Hugunin
2018-03-22bool option -> (VernacCumulative | VernacNonCumulative) optionGaëtan Gilbert
2018-03-21Make parsing independent of the cumulativity flag.Gaëtan Gilbert
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-03-08Merge PR #6909: Deprecate Focus and UnfocusMaxime Dénès
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-03-05Deprecate Focus and Unfocus.Théo Zimmermann
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-04Merge PR #6736: [toplevel] Move beautify to its own pass.Maxime Dénès
2018-03-02Remove 8.5 compatibility support.Théo Zimmermann
2018-03-02Remove VOld compatibility flag.Théo Zimmermann
2018-03-01Merge PR #6864: Remove empty, wrongly located, doc file.Maxime Dénès
2018-02-28[toplevel] Move beautify to its own pass.Emilio Jesus Gallego Arias
2018-02-28Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_...Maxime Dénès
2018-02-28Remove empty, wrongly located, doc file.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:44:13 +0000