diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 5275d04c7c..4c58edf595 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -452,7 +452,7 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk let goals' = List.concat (List.map (fun (gls,v) -> gls) res) in let v' s' pfs' : proof_tree = let (newpfs, rest) = List.fold_left (fun (newpfs,pfs') (gls,v) -> - let before, after = list_split_at (List.length gls) pfs' in + let before, after = list_chop (List.length gls) pfs' in (v s' before :: newpfs, after)) ([], pfs') res in assert(rest = []); v s' (List.rev newpfs) |