diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 8 | ||||
| -rw-r--r-- | printing/pptactic.ml | 2 | ||||
| -rw-r--r-- | printing/prettyp.ml | 4 | ||||
| -rw-r--r-- | printing/printer.ml | 4 |
4 files changed, 9 insertions, 9 deletions
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 ") ++ |