aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* 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 Print Ltac to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Tactic Notation to an EXTEND based command.Gravatar Pierre-Marie Pédrot2016-03-20
* Moving Tacinterp to Hightactics.Gravatar Pierre-Marie Pédrot2016-03-20
* Fixing compilation with old versions of CAMLP5.Gravatar Pierre-Marie Pédrot2016-03-19
* Further reducing the dependencies of the EXTEND macros.Gravatar Pierre-Marie Pédrot2016-03-19
* Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* Moving the parsing of the Ltac proof mode to G_ltac.Gravatar Pierre-Marie Pédrot2016-03-19
* 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
* Making the EXTEND macros almost self-contained.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
* Adopting the same rules for interpreting @, abbreviations andGravatar Hugo Herbelin2016-03-13
* Supporting "(@foo) args" in patterns, where "@foo" has no arguments.Gravatar Hugo Herbelin2016-03-13
* Moving Autorewrite to Hightatctic.Gravatar Pierre-Marie Pédrot2016-03-06
* Fixing bug #4610: Fails to build with camlp4 since the TACTIC EXTEND move.Gravatar Pierre-Marie Pédrot2016-03-06
* Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].Gravatar Pierre-Marie Pédrot2016-03-04
* Exchanging roles of tactic_arg and tactic_top_or_arg entries.Gravatar Pierre-Marie Pédrot2016-03-04
* Removing the UConstr entry of the tactic_arg AST.Gravatar Pierre-Marie Pédrot2016-03-04
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Uniformizing the parsing of argument scopes in Ltac.Gravatar Pierre-Marie Pédrot2016-03-04
* Moving the "move" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "exists" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "symmetry" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "generalize dependent" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "clearbody" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "clear" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "cofix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Moving the "fix" tactic to TACTIC EXTEND.Gravatar Pierre-Marie Pédrot2016-02-29
* Removing the METAIDENT token, as it is not used anymore.Gravatar Pierre-Marie Pédrot2016-02-24
* Removing the MetaIdArg entry of tactic expressions.Gravatar Pierre-Marie Pédrot2016-02-24
* 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
|\|
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | 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
* | ML extensions use untyped representation of user entries.Gravatar Pierre-Marie Pédrot2016-01-17
* | Separating the parsing of user-defined entries from their intepretation.Gravatar Pierre-Marie Pédrot2016-01-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 19:42:13 +0000