Moving Utils.list_* to a proper CList module, which includes stdlib

List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 13 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 0556f6d77f..e1bbcf9c75 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