aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml
Commit message (Expand)AuthorAge
...
* Removing dynamic entries from Pcoq.Gravatar Pierre-Marie Pédrot2016-01-17
* Separating the parsing of user-defined entries from their intepretation.Gravatar Pierre-Marie Pédrot2016-01-16
* Less type-unsafety in Pcoq.Gravatar Pierre-Marie Pédrot2016-01-16
* Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
* Adding a token "index" representing positions (1st, 2nd, etc.).Gravatar Hugo Herbelin2015-12-15
* Fixing the return type of the Atoken symbol.Gravatar Pierre-Marie Pédrot2015-10-28
* Removing unused code in Pcoq.Gravatar Pierre-Marie Pédrot2015-10-27
* Finer type for Pcoq.interp_entry_name.Gravatar Pierre-Marie Pédrot2015-10-27
* Indexing existentially quantified entries returned by interp_entry_name.Gravatar Pierre-Marie Pédrot2015-10-27
* Type-safe grammar extensions.Gravatar Pierre-Marie Pédrot2015-10-27
* Pcoq entries are given a proper module.Gravatar Pierre-Marie Pédrot2015-10-26
* Getting rid of the Atactic entry.Gravatar Pierre-Marie Pédrot2015-10-25
* Getting rid of the Agram entry.Gravatar Pierre-Marie Pédrot2015-10-25
* Pcoq.prod_entry_key now uses a GADT to statically enforce typedness.Gravatar Pierre-Marie Pédrot2015-10-21
* Turn Pcoq into a regular ML file.Gravatar Pierre-Marie Pédrot2015-10-21
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-13 05:30:44 +0000