diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/extraction/extract_env.ml | 2 | ||||
| -rw-r--r-- | contrib/subtac/subtac_pretyping.ml | 7 |
2 files changed, 1 insertions, 8 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 831f31b188..39e2770819 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -161,7 +161,7 @@ let env_for_mtb_with env mtb idl = | _ -> assert false in let l = label_of_id (List.hd idl) in - let before = fst (list_split_at (fun (l',_) -> l=l') sig_b) in + let before = fst (list_split_when (fun (l',_) -> l=l') sig_b) in Modops.add_signature (MPself msid) before env (* From a [structure_body] (i.e. a list of [structure_field_body]) diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index f65e3f786d..0159de5427 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -84,13 +84,6 @@ let find_with_index x l = | [] -> raise Not_found in aux 0 l -let list_split_at index l = - let rec aux i acc = function - hd :: tl when i = index -> (List.rev acc), tl - | hd :: tl -> aux (succ i) (hd :: acc) tl - | [] -> failwith "list_split_at: Invalid argument" - in aux 0 [] l - open Vernacexpr let coqintern_constr evd env : Topconstr.constr_expr -> Rawterm.rawconstr = Constrintern.intern_constr (evars_of evd) env |