aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
Commit message (Expand)AuthorAge
* Generate parsing rules for ML tactics in the same order as before a7917a32.Gravatar Pierre-Marie Pédrot2016-05-02
* Useless code in Tacentries.Gravatar Pierre-Marie Pédrot2016-05-02
* Revert "In the short term, stronger invariant on the syntax of TacAssert, what"Gravatar Hugo Herbelin2016-04-27
* Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing printers for pr_auto_using and pr_firstorder_using."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing parsing of constr argument of ltac functions at level 8 in the"Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing Add Parametric Relation by adding printer for binders."Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing printing of Register retroknowledge."Gravatar Hugo Herbelin2016-04-27
* Revert "A fix to #3709: ensuring extra parentheses when a tactic entry has a"Gravatar Hugo Herbelin2016-04-27
* Revert "Passing around the precedence to the generic printer so as to solve"Gravatar Hugo Herbelin2016-04-27
* Revert "When interpreting "match goal with ... end" in ltac, expand evars by"Gravatar Hugo Herbelin2016-04-27
* Revert "Fixing space in an error message."Gravatar Hugo Herbelin2016-04-27
* Revert "Typo in comment."Gravatar Hugo Herbelin2016-04-27
* Revert "Revert "Honor parsing and printing levels for tactic entry in TACTIC ...Gravatar Hugo Herbelin2016-04-27
* Revert "Honor parsing and printing levels for tactic entry in TACTIC EXTEND and"Gravatar Hugo Herbelin2016-04-27
* Typo in comment.Gravatar Hugo Herbelin2016-04-27
* Fixing space in an error message.Gravatar Hugo Herbelin2016-04-27
* When interpreting "match goal with ... end" in ltac, expand evars byGravatar Hugo Herbelin2016-04-27
* Passing around the precedence to the generic printer so as to solveGravatar Hugo Herbelin2016-04-27
* A fix to #3709: ensuring extra parentheses when a tactic entry has aGravatar Hugo Herbelin2016-04-27
* Fixing printing of Register retroknowledge.Gravatar Hugo Herbelin2016-04-27
* Fixing Add Parametric Relation by adding printer for binders.Gravatar Hugo Herbelin2016-04-27
* Fixing parsing of constr argument of ltac functions at level 8 in theGravatar Hugo Herbelin2016-04-27
* Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-04-27
* Honor parsing and printing levels for tactic entry in TACTIC EXTEND andGravatar Hugo Herbelin2016-04-27
* In the short term, stronger invariant on the syntax of TacAssert, whatGravatar Hugo Herbelin2016-04-27
* Attempt to slightly improve abusive "Collision between boundGravatar Hugo Herbelin2016-04-27
* Merging the ML tactic notation and plain Tactic Notation mechanisms.Gravatar Pierre-Marie Pédrot2016-04-25
* Factorizing code in tactic notations.Gravatar Pierre-Marie Pédrot2016-04-25
* Documenting API.Gravatar Pierre-Marie Pédrot2016-04-25
* Remove dead registering code in Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Disentangle tactic notation resolution from Pcoq.Gravatar Pierre-Marie Pédrot2016-04-24
* Higher-level API for tactic notations.Gravatar Pierre-Marie Pédrot2016-04-24
* Factorizing the declaration of ML notation printing in Tacentries.Gravatar Pierre-Marie Pédrot2016-04-24
* Moving and enhancing the grammar_tactic_prod_item_expr type.Gravatar Pierre-Marie Pédrot2016-04-14
* Adding toplevel representation sharing for some generic arguments.Gravatar Pierre-Marie Pédrot2016-04-12
* Removing redundant *_TYPED AS clauses in EXTEND statements.Gravatar Pierre-Marie Pédrot2016-04-12
* Removing the ad-hoc tactic_expr type.Gravatar Pierre-Marie Pédrot2016-04-11
* Removing extra spaces in printing arguments of VERNAC EXTEND.Gravatar Hugo Herbelin2016-04-09
* Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...Gravatar Hugo Herbelin2016-04-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-04-09
* Fixing printing of toplevel values.Gravatar Pierre-Marie Pédrot2016-04-08
* Getting rid of the "_mods" parsing entry.Gravatar Pierre-Marie Pédrot2016-04-01
* Moving the code handling tactic notations to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
* Moving the Tactic Notation entry parser from Pcoq to Tacentries.Gravatar Pierre-Marie Pédrot2016-03-31
* Fixing an incorrect use of prod_appvect on a term which was not aGravatar Hugo Herbelin2016-03-28
* Fixing an evar leak in Rewrite introduced by 968dfdb15.Gravatar Pierre-Marie Pédrot2016-03-28
* Moving Autorewrite back to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
* Making Autorewrite independent from Ltac.Gravatar Pierre-Marie Pédrot2016-03-25
* Moving Eqdecide to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 18:34:13 +0000