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

5 files changed, 16 insertions, 16 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 488c425cc5..b3fdd384a8 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -97,7 +97,7 @@ let make_constr_action
 	failwith "Unexpected entry of type cases pattern")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
-      let heads,constrs = list_chop n constrs in
+      let heads,constrs = List.chop n constrs in
       let constrlists =
 	if b then (heads@List.hd constrlists)::List.tl constrlists
 	else heads::constrlists
@@ -145,7 +145,7 @@ let make_cases_pattern_action
         anomaly "Unexpected entry of type cases pattern or other")
   | GramConstrListMark (n,b) :: tl ->
       (* Rebuild expansions of ConstrList *)
-      let heads,env = list_chop n env in
+      let heads,env = List.chop n env in
       if b then
         make (env,(heads@List.hd envlist)::List.tl envlist,hasbinders) tl
       else
@@ -278,7 +278,7 @@ let freeze () = (!grammar_state, Lexer.freeze ())
 (* We compare the current state of the grammar and the state to unfreeze,
    by computing the longest common suffixes *)
 let factorize_grams l1 l2 =
-  if l1 == l2 then ([], [], l1) else list_share_tails l1 l2
+  if l1 == l2 then ([], [], l1) else List.share_tails l1 l2
 
 let number_of_entries gcl =
   List.fold_left (fun n (p,_) -> n + p) 0 gcl
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 77c86ad920..f62be2f5c5 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -77,18 +77,18 @@ let check_for_coloneq =
   Gram.Entry.of_parser "lpar_id_colon"
     (fun strm ->
       let rec skip_to_rpar p n =
-	match get_tok (list_last (Stream.npeek n strm)) with
+	match get_tok (List.last (Stream.npeek n strm)) with
         | KEYWORD "(" -> skip_to_rpar (p+1) (n+1)
         | KEYWORD ")" -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1)
 	| KEYWORD "." -> err ()
 	| _ -> skip_to_rpar p (n+1) in
       let rec skip_names n =
-	match get_tok (list_last (Stream.npeek n strm)) with
+	match get_tok (List.last (Stream.npeek n strm)) with
         | IDENT _ | KEYWORD "_" -> skip_names (n+1)
 	| KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *)
 	| _ -> err () in
       let rec skip_binders n =
-	match get_tok (list_last (Stream.npeek n strm)) with
+	match get_tok (List.last (Stream.npeek n strm)) with
         | KEYWORD "(" -> skip_binders (skip_names (n+1))
         | IDENT _ | KEYWORD "_" -> skip_binders (n+1)
 	| KEYWORD ":=" -> ()
@@ -114,7 +114,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
         [([_],_,_)], None -> 1
       | _, Some x ->
           let ids = List.map snd (List.flatten (List.map pi1 bl)) in
-          (try list_index (snd x) ids
+          (try List.index (snd x) ids
           with Not_found -> error "No such fix variable.")
       | _ -> error "Cannot guess decreasing argument of fix." in
   (id,n,CProdN(loc,bl,ty))
@@ -164,7 +164,7 @@ let mkCLambdaN_simple bl c =
     let loc = Loc.merge (fst (List.hd (pi1 (List.hd bl)))) (Constrexpr_ops.constr_loc c) in
     mkCLambdaN_simple_loc loc bl c
 
-let loc_of_ne_list l = Loc.merge (fst (List.hd l)) (fst (list_last l))
+let loc_of_ne_list l = Loc.merge (fst (List.hd l)) (fst (List.last l))
 
 let map_int_or_var f = function
   | ArgArg x -> ArgArg (f x)
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 587e272ddc..1527fa64b8 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -148,17 +148,17 @@ let rec interp_xml_constr = function
   | XmlTag (loc,"VAR",al,[]) ->
       error "XML parser: unable to interp free variables"
   | XmlTag (loc,"LAMBDA",al,(_::_ as xl)) ->
-      let body,decls = list_sep_last xl in
+      let body,decls = List.sep_last xl in
       let ctx = List.map interp_xml_decl decls in
       List.fold_right (fun (na,t) b -> GLambda (loc, na, Explicit, t, b))
 	ctx (interp_xml_target body)
   | XmlTag (loc,"PROD",al,(_::_ as xl)) ->
-      let body,decls = list_sep_last xl in
+      let body,decls = List.sep_last xl in
       let ctx = List.map interp_xml_decl decls in
       List.fold_right (fun (na,t) b -> GProd (loc, na, Explicit, t, b))
 	ctx (interp_xml_target body)
   | XmlTag (loc,"LETIN",al,(_::_ as xl)) ->
-      let body,defs = list_sep_last xl in
+      let body,defs = List.sep_last xl in
       let ctx = List.map interp_xml_def defs in
       List.fold_right (fun (na,t) b -> GLetIn (loc, na, t, b))
         ctx (interp_xml_target body)
@@ -176,7 +176,7 @@ let rec interp_xml_constr = function
       let p = interp_xml_patternsType x in
       let tm = interp_xml_inductiveTerm y in
       let vars = compute_branches_lengths ind in
-      let brs = list_map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl
+      let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl
       in
       let mat = simple_cases_matrix_of_branches ind brs in
       let nparams,n = compute_inductive_nargs ind in
@@ -188,11 +188,11 @@ let rec interp_xml_constr = function
       GRef (loc, ConstructRef (get_xml_constructor al))
   | XmlTag (loc,"FIX",al,xl) ->
       let li,lnct = List.split (List.map interp_xml_FixFunction xl) in
-      let ln,lc,lt = list_split3 lnct in
+      let ln,lc,lt = List.split3 lnct in
       let lctx = List.map (fun _ -> []) ln in
       GRec (loc, GFix (Array.of_list li, get_xml_noFun al), Array.of_list ln, Array.of_list lctx, Array.of_list lc, Array.of_list lt)
   | XmlTag (loc,"COFIX",al,xl) ->
-      let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
+      let ln,lc,lt = List.split3 (List.map interp_xml_CoFixFunction xl) in
       GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
   | XmlTag (loc,"CAST",al,[x1;x2]) ->
       GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2))
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 14644339cd..f277acfd15 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -402,7 +402,7 @@ and progress_utf8 last nj n c tt cs =
     if n=1 then
       update_longest_valid_token last (nj+n) tt cs
     else
-      match Util.list_skipn (nj+1) (Stream.npeek (nj+n) cs) with
+      match Util.List.skipn (nj+1) (Stream.npeek (nj+n) cs) with
       | l when List.length l = n-1 ->
 	 List.iter (check_utf8_trailing_byte cs) l;
 	 let tt = List.fold_left (fun tt c -> CharMap.find c tt.branch) tt l in
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 4df8d94903..8fef987e6a 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -538,7 +538,7 @@ let find_position_gen forpat ensure assoc lev =
 	    Some (Level (constr_level n)), None, None, None
 
 let remove_levels n =
-  level_stack := list_skipn n !level_stack
+  level_stack := List.skipn n !level_stack
 
 let rec list_mem_assoc_triple x = function
   | [] -> false