aboutsummaryrefslogtreecommitdiff
path: root/ltac
AgeCommit message (Expand)Author
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-08-30 01:08:44 +0000