diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0556f6d77..e1bbcf9c7 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -193,7 +193,7 @@ let parse_ind_args si args relmax = let oib_equal o1 o2 = id_ord o1.mind_typename o2.mind_typename = 0 && - list_equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && + List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt && begin match o1.mind_arity, o2.mind_arity with | Monomorphic {mind_user_arity=c1; mind_sort=s1}, Monomorphic {mind_user_arity=c2; mind_sort=s2} -> @@ -206,10 +206,10 @@ let mib_equal m1 m2 = m1.mind_record = m2.mind_record && m1.mind_finite = m2.mind_finite && m1.mind_ntypes = m2.mind_ntypes && - list_equal eq_named_declaration m1.mind_hyps m2.mind_hyps && + List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps && m1.mind_nparams = m2.mind_nparams && m1.mind_nparams_rec = m2.mind_nparams_rec && - list_equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt && + List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt && m1.mind_constraints = m2.mind_constraints (*S Extraction of a type. *) @@ -439,7 +439,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) | _ -> [] in let field_names = - list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in + List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in assert (List.length field_names = List.length typ); let projs = ref Cset.empty in let mp,d,_ = repr_mind kn in @@ -674,7 +674,7 @@ and extract_cst_app env mle mlt kn args = let mla = if not magic1 then try - let l,l' = list_chop (projection_arity (ConstRef kn)) mla in + let l,l' = List.chop (projection_arity (ConstRef kn)) mla in if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l' else mla with _ -> mla @@ -697,7 +697,7 @@ and extract_cst_app env mle mlt kn args = (* Partially applied function with some logical arg missing. We complete via eta and expunge logical args. *) let ls' = ls-la in - let s' = list_skipn la s in + let s' = List.skipn la s in let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in let e = anonym_or_dummy_lams (mlapp head mla) s' in put_magic_if magic2 (remove_n_lams (List.length optdummy) e) @@ -729,7 +729,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = let la = List.length args in assert (la <= ls + params_nb); let la' = max 0 (la - params_nb) in - let args' = list_lastn la' args in + let args' = List.lastn la' args in (* Now, we build the expected type of the constructor *) let metas = List.map new_meta args' in (* If stored and expected types differ, then magic! *) @@ -758,7 +758,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = then put_magic_if (magic2 && not magic1) (head mla) else (* [ params_nb <= la <= ls + params_nb ] *) let ls' = params_nb + ls - la in - let s' = list_lastn ls' s in + let s' = List.lastn ls' s in let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in put_magic_if magic2 (anonym_or_dummy_lams (head mla) s') @@ -847,7 +847,7 @@ let decomp_lams_eta_n n m env c t = let rels',c = decompose_lam c in let d = n - m in (* we'd better keep rels' as long as possible. *) - let rels = (list_firstn d rels) @ rels' in + let rels = (List.firstn d rels) @ rels' in let eta_args = List.rev_map mkRel (interval 1 d) in rels, applist (lift d c,eta_args) @@ -886,7 +886,7 @@ let extract_std_constant env kn body typ = and m = nb_lam body in if n <= m then decompose_lam_n n body else - let s,s' = list_chop m s in + let s,s' = List.chop m s in if List.for_all ((=) Keep) s' && (lang () = Haskell || sign_kind s <> UnsafeLogicalSig) then decompose_lam_n m body @@ -895,7 +895,7 @@ let extract_std_constant env kn body typ = (* Should we do one eta-expansion to avoid non-generalizable '_a ? *) let rels, c = let n = List.length rels in - let s,s' = list_chop n s in + let s,s' = List.chop n s in let k = sign_kind s in let empty_s = (k = EmptySig || k = SafeLogicalSig) in if lang () = Ocaml && empty_s && not (gentypvar_ok c) @@ -904,8 +904,8 @@ let extract_std_constant env kn body typ = else rels,c in let n = List.length rels in - let s = list_firstn n s in - let l,l' = list_chop n l in + let s = List.firstn n s in + let l,l' = List.chop n l in let t' = type_recomp (l',t') in (* The initial ML environment. *) let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in |