aboutsummaryrefslogtreecommitdiff
path: root/ltac
AgeCommit message (Expand)Author
2016-04-27Attempt to slightly improve abusive "Collision between boundHugo Herbelin
2016-04-25Merging the ML tactic notation and plain Tactic Notation mechanisms.Pierre-Marie Pédrot
2016-04-25Factorizing code in tactic notations.Pierre-Marie Pédrot
2016-04-25Documenting API.Pierre-Marie Pédrot
2016-04-24Remove dead registering code in Pcoq.Pierre-Marie Pédrot
2016-04-24Disentangle tactic notation resolution from Pcoq.Pierre-Marie Pédrot
2016-04-24Higher-level API for tactic notations.Pierre-Marie Pédrot
2016-04-24Factorizing the declaration of ML notation printing in Tacentries.Pierre-Marie Pédrot
2016-04-14Moving and enhancing the grammar_tactic_prod_item_expr type.Pierre-Marie Pédrot
2016-04-12Adding toplevel representation sharing for some generic arguments.Pierre-Marie Pédrot
2016-04-12Removing redundant *_TYPED AS clauses in EXTEND statements.Pierre-Marie Pédrot
2016-04-11Removing the ad-hoc tactic_expr type.Pierre-Marie Pédrot
2016-04-09Removing extra spaces in printing arguments of VERNAC EXTEND.Hugo Herbelin
2016-04-09Re-add printer for tacdef_body so that Ltac definitions are printed by pr_ver...Hugo Herbelin
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-04-08Fixing printing of toplevel values.Pierre-Marie Pédrot
2016-04-01Getting rid of the "_mods" parsing entry.Pierre-Marie Pédrot
2016-03-31Moving the code handling tactic notations to Tacentries.Pierre-Marie Pédrot
2016-03-31Moving the Tactic Notation entry parser from Pcoq to Tacentries.Pierre-Marie Pédrot
2016-03-28Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
2016-03-28Fixing an evar leak in Rewrite introduced by 968dfdb15.Pierre-Marie Pédrot
2016-03-25Moving Autorewrite back to tactics/.Pierre-Marie Pédrot
2016-03-25Making Autorewrite independent from Ltac.Pierre-Marie Pédrot
2016-03-25Moving Eqdecide to tactics/.Pierre-Marie Pédrot
2016-03-25Making Eqdecide independent of Extratactics.Pierre-Marie Pédrot
2016-03-25Moving Eauto and Class_tactics to tactics/.Pierre-Marie Pédrot
2016-03-25Moving type_uconstr to Pretyping.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-02 02:56:00 +0000