aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
Commit message (Expand)AuthorAge
* [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
* Type-safe constr notations.Gravatar Pierre-Marie Pédrot2016-05-10
* Purer implementation of empty level registering in Pcoq.Gravatar Pierre-Marie Pédrot2016-05-10
* Removing the Entry module now that rules need not be marshalled.Gravatar Pierre-Marie Pédrot2016-05-10
* Hardening the obsolete unsafe_grammar_statement API.Gravatar Pierre-Marie Pédrot2016-05-10
* Removing dead code in Compat.Gravatar Pierre-Marie Pédrot2016-05-10
* Remove dead registering code in Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Moving the Tactic Notation entry parser from Pcoq to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
* Moving the Ltac definition command to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving the proof mode parsing management to Pcoq.Gravatar Pierre-Marie Pédrot2016-03-19
* Do not export entry_key from Pcoq anymore.Gravatar Pierre-Marie Pédrot2016-03-19
* Simplifying the code of Entry.Gravatar Pierre-Marie Pédrot2016-03-19
* Removing dead code in Pcoq.Gravatar Pierre-Marie Pédrot2016-03-18
* ARGUMENT EXTEND made of only one entry share the same grammar.Gravatar Pierre-Marie Pédrot2016-03-18
* Removing the special status of generic arguments defined by Coq itself.Gravatar Pierre-Marie Pédrot2016-03-17
* Adding a universe argument to Pcoq.create_generic_entry.Gravatar Pierre-Marie Pédrot2016-03-17
* Relying on parsing rules rather than genarg to check if an argument is empty.Gravatar Pierre-Marie Pédrot2016-03-17
* Removing a source of type-unsafeness in Pcoq.Gravatar Pierre-Marie Pédrot2016-02-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 12:33:57 +0000