aboutsummaryrefslogtreecommitdiff
path: root/ltac/tacinterp.ml
AgeCommit message (Expand)Author
2016-04-27Attempt to slightly improve abusive "Collision between boundHugo Herbelin
2016-04-11Removing the ad-hoc tactic_expr type.Pierre-Marie Pédrot
2016-04-08Fixing printing of toplevel values.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