aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/change.v
AgeCommit message (Expand)Author
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
2019-05-03Tactics: fixing "change_no_check in".Hugo Herbelin
2019-04-30Mini-test.Hugo Herbelin
2017-05-19Fixing an extra bug with pattern_of_constr.Hugo Herbelin
2014-11-16Fixing side bug in db37c9f3f32ae7 delaying interpretation of theHugo Herbelin
2014-10-16Relaxing again the test on types of replacements in tactic changeHugo Herbelin
2014-09-19Fixing #3641 (loop in e_contextually, introduced in r16525).Hugo Herbelin
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2011-10-05It happens that the type inference algorithm (pretyping) did not checkherbelin
2009-12-30Fixing bug #2146 (broken selection of occurrences in "change").herbelin
2009-12-24In "simpl c" and "change c with d", c can be a pattern.herbelin
2008-02-06Correction d'un bug à l'interprétation de "change" (on exigeait queherbelin