aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
Commit message (Expand)AuthorAge
* 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
* | Less type-unsafety in Pcoq.Gravatar Pierre-Marie Pédrot2016-01-16
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
* | Continuing 003fe3d5e on parsing positions.Gravatar Hugo Herbelin2016-01-14
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | Remove some useless type declarations.Gravatar Guillaume Melquiond2016-01-02
* | Simplification of grammar_prod_item type.Gravatar Pierre-Marie Pédrot2016-01-02
* | Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* | Removing unused parsing entries.Gravatar Pierre-Marie Pédrot2015-12-28
* | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlGravatar Hugo Herbelin2015-12-25
* | Fixing non exhaustive pattern-matching in 003fe3d5e60b.Gravatar Hugo Herbelin2015-12-25
* | Removing auto from the tactic AST.Gravatar Pierre-Marie Pédrot2015-12-24
* | Partial backtrack on commit 20641795624.Gravatar Pierre-Marie Pédrot2015-12-23
* | CLEANUP: the definition of the "Constrexpr.case_expr" type was simplifiedGravatar Matej Kosik2015-12-18
* | CLEANUP: Vernacexpr.VernacDeclareTacticDefinitionGravatar Matej Kosik2015-12-18
* | ALPHA-CONVERSION: in "parsing/g_vernac.ml4" fileGravatar Matej Kosik2015-12-18
* | CLEANUP: Vernacexpr.vernac_exprGravatar Matej Kosik2015-12-18
* | Adding a token "index" representing positions (1st, 2nd, etc.).Gravatar Hugo Herbelin2015-12-15
* | Tactics: Generalizing the use of the experimental clearing modifier toGravatar Hugo Herbelin2015-12-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
|\|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 23:36:18 +0000