aboutsummaryrefslogtreecommitdiff
path: root/ltac/rewrite.ml
AgeCommit message (Collapse)Author
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-04Getting rid of the Geninterp.generic_interp function.Pierre-Marie Pédrot
2016-04-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-28Fixing an incorrect use of prod_appvect on a term which was not aHugo Herbelin
product in setoid_rewrite. Before commit e8c47b652, it was raising an error which has been turned to an anomaly. This impacted Compcert where the former error was (apparently) caught so that setoid_rewrite was returning back to ordinary rewrite.
2016-03-28Fixing an evar leak in Rewrite introduced by 968dfdb15.Pierre-Marie Pédrot
2016-03-25Making Autorewrite independent from Ltac.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot