From f8394a52346bf1e6f98e7161e75fb65bd0631391 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Sep 2012 16:17:09 +0000 Subject: 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 --- printing/ppconstr.ml | 8 ++++---- printing/pptactic.ml | 2 +- printing/prettyp.ml | 4 ++-- printing/printer.ml | 4 ++-- 4 files changed, 9 insertions(+), 9 deletions(-) (limited to 'printing') diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index f99d8c109f..190181c23f 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -460,8 +460,8 @@ let pr pr sep inherited a = pr spc ltop b), lletin | CAppExpl (_,(Some i,f),l) -> - let l1,l2 = list_chop i l in - let c,l1 = list_sep_last l1 in + let l1,l2 = List.chop i l in + let c,l1 = List.sep_last l1 in let p = pr_proj (pr mt) pr_appexpl c f l1 in if l2<>[] then p ++ prlist (pr spc (lapp,L)) l2, lapp @@ -473,8 +473,8 @@ let pr pr sep inherited a = hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg | CAppExpl (_,(None,f),l) -> pr_appexpl (pr mt) f l, lapp | CApp (_,(Some i,f),l) -> - let l1,l2 = list_chop i l in - let c,l1 = list_sep_last l1 in + let l1,l2 = List.chop i l in + let c,l1 = List.sep_last l1 in assert (snd c = None); let p = pr_proj (pr mt) pr_app (fst c) f l1 in if l2<>[] then diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7118388cb9..1a8f713971 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -592,7 +592,7 @@ let pr_fix_tac (id,n,c) = let rec set_nth_name avoid n = function (nal,ty)::bll -> if n <= List.length nal then - match list_chop (n-1) nal with + match List.chop (n-1) nal with _, (_,Name id) :: _ -> id, (nal,ty)::bll | bef, (loc,Anonymous) :: aft -> let id = next_ident_away (id_of_string"y") avoid in diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 86b2da2eb0..7fbbc0a2ec 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -93,7 +93,7 @@ let print_impargs_by_name max = function let print_one_impargs_list l = let imps = List.filter is_status_implicit l in let maximps = List.filter Impargs.maximal_insertion_of imps in - let nonmaximps = list_subtract imps maximps in + let nonmaximps = List.subtract imps maximps in print_impargs_by_name false nonmaximps @ print_impargs_by_name true maximps @@ -127,7 +127,7 @@ let need_expansion impl ref = let ctx = (prod_assum typ) in let nprods = List.length (List.filter (fun (_,b,_) -> b=None) ctx) in impl <> [] & List.length impl >= nprods & - let _,lastimpl = list_chop nprods impl in + let _,lastimpl = List.chop nprods impl in List.filter is_status_implicit lastimpl <> [] let print_impargs ref = diff --git a/printing/printer.ml b/printing/printer.ml index 70a90b8ea6..1ad9dba499 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -289,7 +289,7 @@ let pr_concl n sigma g = (* display evar type: a context and a type *) let pr_evgl_sign gl = let ps = pr_named_context_of (evar_unfiltered_env gl) in - let _,l = list_filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in + let _,l = List.filter2 (fun b c -> not b) (evar_filter gl,evar_context gl) in let ids = List.rev (List.map pi1 l) in let warn = if ids = [] then mt () else @@ -664,7 +664,7 @@ let print_one_inductive env mib ((_,i) as ind) = brk(0,2) ++ print_constructors envpar mip.mind_consnames cstrtypes let print_mutual_inductive env mind mib = - let inds = list_tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets) + let inds = List.tabulate (fun x -> (mind,x)) (Array.length mib.mind_packets) in hov 0 ( str (if mib.mind_finite then "Inductive " else "CoInductive ") ++ -- cgit v1.2.3