diff options
Diffstat (limited to 'tactics/refine.ml')
| -rw-r--r-- | tactics/refine.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/refine.ml b/tactics/refine.ml index fc2da8d0a..1cb4f01e2 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -348,7 +348,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = | _ -> error "Recursive functions must have names." in let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in - let firsts,lasts = list_chop j (Array.to_list fixes) in + let firsts,lasts = List.chop j (Array.to_list fixes) in tclTHENS (tclTHEN (ensure_products (succ ni.(j))) @@ -365,7 +365,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl = | _ -> error "Recursive functions must have names." in let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in - let firsts,lasts = list_chop j (Array.to_list cofixes) in + let firsts,lasts = List.chop j (Array.to_list cofixes) in tclTHENS (mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j) (List.map (function |