diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index aa13d27b1..bd304d975 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -49,7 +49,7 @@ let introCaseAssumsThen tac ba = (ba.branchnames, []), if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in let introCaseAssums = - tclTHEN (intros_pattern no_move l1) (intros_clearing l3) in + tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) (* The following tactic Decompose repeatedly applies the |