aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
Commit message (Expand)AuthorAge
* Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24
* 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
* Fix bug #4869, allow Prop, Set, and level names in constraints.Gravatar Matthieu Sozeau2016-09-29
* 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
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Removing dynamic entries from Pcoq.Gravatar Pierre-Marie Pédrot2016-01-17
* | ML extensions use untyped representation of user entries.Gravatar Pierre-Marie Pédrot2016-01-17
* | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
* | 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
* | Expliciting some uses of Compat module.Gravatar Pierre-Marie Pédrot2015-10-21
|/
* grammar: export constr_evalGravatar Enrico Tassi2015-03-30
* grammar: export hypidentGravatar Enrico Tassi2015-03-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-04 07:09:39 +0000