aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
Commit message (Expand)AuthorAge
* Introduce a Pcoq.Entry module for functions that ought to be exported.Gravatar Pierre-Marie Pédrot2018-07-07
* Remove dead code that used to be there for CamlpX compatibility.Gravatar Pierre-Marie Pédrot2018-07-07
* Fix compilation of Coq with camlp5 master branch.Gravatar Pierre-Marie Pédrot2018-07-06
* Use a homebrew parser to replace the GEXTEND extension points of Camlp5.Gravatar Pierre-Marie Pédrot2018-06-29
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* Statment -> StatementGravatar Hugo Herbelin2018-06-03
* [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
* [api] Move universe syntax to `Glob_term`Gravatar Emilio Jesus Gallego Arias2018-05-08
* [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Emilio Jesus Gallego Arias2018-04-26
* [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
* 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
* | Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ | |/ |/|
* | [toplevel] Move beautify to its own pass.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Moving Metasyntax.register_grammar to Pcoq for usability in Egramcoq.Gravatar Hugo Herbelin2018-02-20
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
* [summary] Allow typed projections from global state + rework of internals.Gravatar Emilio Jesus Gallego Arias2017-12-09
* Remove pidentref grammar entry.Gravatar Gaëtan Gilbert2017-11-20
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Merge PR #1051: Using an algebraic type for distinguishing toplevel input fro...Gravatar Maxime Dénès2017-09-15
|\
| * Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
* | Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* G_prim: the bigint entry keeps numbers in raw stringsGravatar Pierre Letouzey2017-06-14
* [location] Use located in misctypes.Gravatar Emilio Jesus Gallego Arias2017-04-24
* [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
* Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
|\
| * don't require printing-only notation to be productiveGravatar Ralf Jung2017-02-16
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\|
| * Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\|
| * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| * Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
* | Moving Ltac-specific parsing API to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-14
|/
* Remove lexing of ordinal notations.Gravatar Maxime Dénès2016-07-03
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* The grammar_extend function now registers unsynchronized extensions.Gravatar Pierre-Marie Pédrot2016-05-11
* Making the grammar command extend API purely functional.Gravatar Pierre-Marie Pédrot2016-05-11
* Moving the constr empty entry registering to the state-based API.Gravatar Pierre-Marie Pédrot2016-05-11
* Turning the grammar extend command API into a state-passing one.Gravatar Pierre-Marie Pédrot2016-05-11
* Moving the grammar summary to Pcoq.Gravatar Pierre-Marie Pédrot2016-05-11
* Delimiting the use of unsafe code in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-06 17:06:43 +0000