aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
Commit message (Expand)AuthorAge
* 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
* Making Eqdecide independent of Extratactics.Gravatar Pierre-Marie Pédrot2016-03-25
* Moving Eauto and Class_tactics to tactics/.Gravatar Pierre-Marie Pédrot2016-03-25
* Moving type_uconstr to Pretyping.Gravatar Pierre-Marie Pédrot2016-03-25
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-04 02:37:07 +0000