aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* Statment -> StatementGravatar Hugo Herbelin2018-06-03
* [notations] Split interpretation and parsing of notationsGravatar Emilio Jesus Gallego Arias2018-05-31
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
* [api] [parsing] Move Egram* to `vernac/`Gravatar Emilio Jesus Gallego Arias2018-05-27
* [api] Move `Vernacexpr` to parsing.Gravatar Emilio Jesus Gallego Arias2018-05-23
* [api] Move `opacity_flag` to `Proof_global`.Gravatar Emilio Jesus Gallego Arias2018-05-23
* [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
* Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Pierre-Marie Pédrot2018-05-04
|\
* | [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
| * [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Emilio Jesus Gallego Arias2018-04-26
|/
* [api] Remove dependency of library on Vernacexpr.Gravatar Emilio Jesus Gallego Arias2018-04-06
* Merge PR #7016: Make parsing independent of the cumulativity flag.Gravatar Enrico Tassi2018-04-05
|\
* \ Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Gravatar Enrico Tassi2018-04-04
|\ \
| * | [stm] Move VernacBacktrack to the toplevel.Gravatar Emilio Jesus Gallego Arias2018-04-01
* | | Remove deprecated commands Arguments Scope and Implicit ArgumentsGravatar Jasper Hugunin2018-03-30
|/ /
| * bool option -> (VernacCumulative | VernacNonCumulative) optionGravatar Gaëtan Gilbert2018-03-22
| * Make parsing independent of the cumulativity flag.Gravatar Gaëtan Gilbert2018-03-21
* | [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
|/
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
* Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\
* \ Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\ \
| * | Allow universe declarations for [with Definition].Gravatar Gaëtan Gilbert2018-03-05
| | * Deprecate Focus and Unfocus.Gravatar Théo Zimmermann2018-03-05
* | | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ | |/ / |/| |
* | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \
* \ \ \ Merge PR #6736: [toplevel] Move beautify to its own pass.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ | |_|_|/ |/| | |
| | * | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | * | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
| |/ / |/| |
* | | Merge PR #6864: Remove empty, wrongly located, doc file.Gravatar Maxime Dénès2018-03-01
|\ \ \
| | * | [toplevel] Move beautify to its own pass.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ / |/| |
* | | Merge PR #6812: Rename release_lexer_state to the more descriptive get_lexer_...Gravatar Maxime Dénès2018-02-28
|\ \ \
| | * | Remove empty, wrongly located, doc file.Gravatar Théo Zimmermann2018-02-28
| |/ / |/| |
| | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
| * Rename release_lexer_state to the more descriptive get_lexer_state.Gravatar Jim Fehrle2018-02-22
* | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* | Trying a hack to support {'pat|P} without breaking compatibility.Gravatar Hugo Herbelin2018-02-20
* | Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
* | Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
* | Notations: A step in cleaning constr_entry_key.Gravatar Hugo Herbelin2018-02-20
* | Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
* | Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* | Adding patterns in the category of binders for notations.Gravatar Hugo Herbelin2018-02-20
* | Renaming binders into binderlists in egramcoq.ml.Gravatar Hugo Herbelin2018-02-20
* | Introducing an intermediary type "constr_prod_entry_key" for grammar producti...Gravatar Hugo Herbelin2018-02-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 11:01:49 +0000