diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index a2ec6dfa5..32acc5af5 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -37,10 +37,10 @@ let introCaseAssumsThen tac ba = let n1 = List.length case_thin_sign in let n2 = List.length ba.branchnames in let (l1,l2),l3 = - if n1 < n2 then list_chop n1 ba.branchnames, [] + if n1 < n2 then List.chop n1 ba.branchnames, [] else (ba.branchnames, []), - if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in + if n1 > n2 then snd (List.chop n2 case_thin_sign) else [] in let introCaseAssums = tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) |