diff options
| author | letouzey | 2010-04-16 14:13:00 +0000 |
|---|---|---|
| committer | letouzey | 2010-04-16 14:13:00 +0000 |
| commit | e960cd8dac76829f3a48167e70a23c65d8dd797f (patch) | |
| tree | 6a4612192d654046872255f98bacf984da949288 /tactics/class_tactics.ml4 | |
| parent | f57a38bb53dc06cef1cee78c60946aa5e6d3cf0b (diff) | |
Util: remove list_split_at which is a clone of list_chop
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/class_tactics.ml4')
| -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) |