aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.ml
Commit message (Expand)AuthorAge
...
* AlistNsep token now accepts an arbitrary separator.Gravatar Pierre-Marie Pédrot2016-05-10
* Simpler data structure for Arules token.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
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
* Remove dead registering code in Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
* Moving the Tactic Notation entry parser from Pcoq to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
* Adding a new Ltac generic argument for forced tactics returing unit.Gravatar Pierre-Marie Pédrot2016-03-20
* 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
* Allowing generalized rules in typed symbols.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
* Code factorization in Pcoq.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
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
* Simplification and type-safety of Pcoq thanks to GADTs in Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* Temporary commit getting rid of Obj.magic unsafety for Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* 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 2024-06-13 21:02:40 +0000