From ddc9c1bd8e1eaae186468f093e467d8f2e1091cd Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 18 Feb 2013 15:42:36 +0000 Subject: use List.rev_map whenever possible git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16211 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/checker.ml | 2 +- checker/include | 2 +- dev/top_printers.ml | 4 ++-- interp/coqlib.ml | 2 +- kernel/nativecode.ml | 2 +- library/declare.ml | 2 +- library/library.ml | 2 +- parsing/egramcoq.ml | 2 +- plugins/extraction/table.ml | 2 +- plugins/firstorder/formula.ml | 2 +- plugins/funind/merge.ml | 4 ++-- plugins/xml/cic2acic.ml | 2 +- plugins/xml/xmlcommand.ml | 4 ++-- pretyping/cases.ml | 2 +- pretyping/indrec.ml | 2 +- pretyping/recordops.ml | 2 +- printing/printer.ml | 2 +- tools/coqdep_common.ml | 2 +- toplevel/auto_ind_decl.ml | 2 +- toplevel/himsg.ml | 2 +- toplevel/mltop.ml | 2 +- 21 files changed, 24 insertions(+), 24 deletions(-) diff --git a/checker/checker.ml b/checker/checker.ml index 42e5b868b..1daf449d8 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -80,7 +80,7 @@ let add_rec_path ~unix_path ~coq_root = let prefix = Dir_path.repr coq_root in let convert_dirs (lp, cp) = try - let path = List.map convert_string (List.rev cp) @ prefix in + let path = List.rev_map convert_string cp @ prefix in Some (lp, Names.Dir_path.make path) with Exit -> None in diff --git a/checker/include b/checker/include index b7d46d4b3..0b68da4b7 100644 --- a/checker/include +++ b/checker/include @@ -127,7 +127,7 @@ let mod_access m fld = ;; let parse_dp s = - make_dirpath(List.map id_of_string (List.rev (Str.split(Str.regexp"\\.") s))) + make_dirpath(List.rev_map id_of_string (Str.split(Str.regexp"\\.") s)) ;; let parse_sp s = let l = List.rev (Str.split(Str.regexp"\\.") s) in diff --git a/dev/top_printers.ml b/dev/top_printers.ml index aa7d82045..9386c82de 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -322,7 +322,7 @@ let print_pure_constr csr = and sp_display sp = (* let dir,l = decode_kn sp in let ls = - match List.rev (List.map Id.to_string (Dir_path.repr dir)) with + match List.rev_map Id.to_string (Dir_path.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l @@ -331,7 +331,7 @@ let print_pure_constr csr = and sp_con_display sp = (* let dir,l = decode_kn sp in let ls = - match List.rev (List.map Id.to_string (Dir_path.repr dir)) with + match List.rev_map Id.to_string (Dir_path.repr dir) with ("Top"::l)-> l | ("Coq"::_::l) -> l | l -> l diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 92a268796..b0a9831b7 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -21,7 +21,7 @@ open Smartlocate type message = string -let make_dir l = Dir_path.make (List.map Id.of_string (List.rev l)) +let make_dir l = Dir_path.make (List.rev_map Id.of_string l) let find_reference locstr dir s = let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 9fee03ca1..04a063044 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -936,7 +936,7 @@ let string_of_label l = Unicode.ascii_of_ident (string_of_label l) let string_of_dirpath = function | [] -> "_" - | sl -> String.concat "_" (List.map string_of_id (List.rev sl)) + | sl -> String.concat "_" (List.rev_map string_of_id sl) (* The first letter of the file name has to be a capital to be accepted by *) (* OCaml as a module identifier. *) diff --git a/library/declare.ml b/library/declare.ml index 27aecfe73..3627df7fe 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -138,7 +138,7 @@ let cache_constant ((sp,kn),(cdt,dhyps,kind)) = let discharged_hyps kn sechyps = let (_,dir,_) = repr_kn kn in let args = Array.to_list (instance_from_variable_context sechyps) in - List.rev (List.map (Libnames.make_path dir) args) + List.rev_map (Libnames.make_path dir) args let discharge_constant ((sp,kn),(cdt,dhyps,kind)) = let con = constant_of_kn kn in diff --git a/library/library.ml b/library/library.ml index e4e687bec..0fdd6d75e 100644 --- a/library/library.ml +++ b/library/library.ml @@ -71,7 +71,7 @@ let add_load_path isroot (phys_path,coq_path) = let extend_path_with_dirpath p dir = List.fold_left Filename.concat p - (List.map Id.to_string (List.rev (Dir_path.repr dir))) + (List.rev_map Id.to_string (Dir_path.repr dir)) let root_paths_matching_dir_path dir = let rec aux = function diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index a53bf630e..eb27c2f4e 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -321,7 +321,7 @@ let unfreeze (grams, lex) = remove_levels n; grammar_state := common; Lexer.unfreeze lex; - List.iter extend_grammar (List.rev (List.map snd redo)) + List.iter extend_grammar (List.rev_map snd redo) let init_grammar () = remove_grammars (number_of_entries !grammar_state); diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 51946871f..9252ae0ec 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -273,7 +273,7 @@ let safe_pr_long_global r = let pr_long_mp mp = let lid = Dir_path.repr (Nametab.dirpath_of_module mp) in - str (String.concat "." (List.map Id.to_string (List.rev lid))) + str (String.concat "." (List.rev_map Id.to_string lid)) let pr_long_global ref = pr_path (Nametab.path_of_global ref) diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 093087511..557e9c25d 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -169,7 +169,7 @@ let build_atoms gl metagen side cciterm = | Hyp -> build_rec [] false cciterm | Hint -> let rels,head=decompose_prod cciterm in - let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in + let env=List.rev_map (fun _->mkMeta (metagen true)) rels in build_rec env false head;trivial:=false (* special for hints *) end; (!trivial, diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 30c60b52b..2c44353f2 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -663,9 +663,9 @@ let build_link_map_aux (allargs1:Id.t array) (allargs2:Id.t array) let build_link_map allargs1 allargs2 lnk = let allargs1 = - Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs1)) in + Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs1) in let allargs2 = - Array.of_list (List.rev (List.map (fun (x,_,_) -> id_of_name x) allargs2)) in + Array.of_list (List.rev_map (fun (x,_,_) -> id_of_name x) allargs2) in build_link_map_aux allargs1 allargs2 lnk diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index 2772779d4..90712c473 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -457,7 +457,7 @@ print_endline "PASSATO" ; flush stdout ; let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in let he1'' = String.concat "/" - (List.map Names.Id.to_string (List.rev he1')) ^ "/" + (List.rev_map Names.Id.to_string he1') ^ "/" ^ (Names.Id.to_string he1_id) ^ ".var" in (he1'',he2)::subst, extra_args, uninst diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 479b04228..91e15e8a6 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -35,7 +35,7 @@ let filter_params pvars hyps = let ids' = id::ids in let ids'' = "cic:/" ^ - String.concat "/" (List.rev (List.map Names.Id.to_string ids')) in + String.concat "/" (List.rev_map Names.Id.to_string ids') in let he' = ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in let tl' = aux ids' tl in @@ -531,7 +531,7 @@ let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ; let uri_of_dirpath dir = "/" ^ String.concat "/" - (List.map Names.Id.to_string (List.rev (Names.Dir_path.repr dir))) + (List.rev_map Names.Id.to_string (Names.Dir_path.repr dir)) ;; let _ = diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 60e3025b4..2910774db 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2135,7 +2135,7 @@ let abstract_tomatch env tomatchs tycon = let build_dependent_signature env evars avoid tomatchs arsign = let avoid = ref avoid in let arsign = List.rev arsign in - let allnames = List.rev (List.map (List.map pi1) arsign) in + let allnames = List.rev_map (List.map pi1) arsign in let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in let eqs, neqs, refls, slift, arsign' = List.fold_left2 diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 60b708f5b..bf166f128 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -183,7 +183,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs = | _ -> assert false else if dep then - let realargs = List.map (fun k -> mkRel (i-k)) (List.rev li) in + let realargs = List.rev_map (fun k -> mkRel (i-k)) li in let params = List.map (lift i) vargs in let co = applist (mkConstruct cs.cs_cstr,params@realargs) in Reduction.beta_appvect c [|co|] diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 777e6c1d8..cc6ec1e95 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -225,7 +225,7 @@ let compute_canonical_projections (con,ind) = let v = mkConst con in let c = Environ.constant_value (Global.env()) con in let lt,t = Reductionops.splay_lam (Global.env()) Evd.empty c in - let lt = List.rev (List.map snd lt) in + let lt = List.rev_map snd lt in let args = snd (decompose_app t) in let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } = lookup_structure ind in diff --git a/printing/printer.ml b/printing/printer.ml index fa776d11e..d0a61bb11 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -297,7 +297,7 @@ let pr_concl n sigma g = let pr_evgl_sign gl = let ps = pr_named_context_of (evar_env 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 ids = List.rev_map pi1 l in let warn = if ids = [] then mt () else (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml index 4977a94cd..235aa3074 100644 --- a/tools/coqdep_common.ml +++ b/tools/coqdep_common.ml @@ -141,7 +141,7 @@ let warning_clash file dir = let f = Filename.basename f1 in let d1 = Filename.dirname f1 in let d2 = Filename.dirname f2 in - let dl = List.map Filename.dirname (List.rev fl) in + let dl = List.rev_map Filename.dirname fl in eprintf "*** Warning: in file %s, \n required library %s matches several files in path\n (found %s.v in " file (String.concat "." dir) f; diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 6e88628bd..3fa932f06 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -42,7 +42,7 @@ and aux = function let deconstruct_type t = let l,r = decompose_prod t in - (List.map (fun (_,b) -> b) (List.rev l))@[r] + (List.rev_map snd l)@[r] exception EqNotFound of inductive * inductive exception EqUnknown of string diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 18638ad8b..c0f1903df 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1052,7 +1052,7 @@ let is_defined_ltac trace = let explain_ltac_call_trace (nrep,last,trace,loc) = let calls = - (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) + (nrep,last) :: List.rev_map (fun(n,_,ck)->(n,ck)) trace in let pr_call (n,ck) = (match ck with diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml index 59059a77a..d5d8b1076 100644 --- a/toplevel/mltop.ml +++ b/toplevel/mltop.ml @@ -174,7 +174,7 @@ let add_rec_path ~unix_path ~coq_root = let prefix = Names.Dir_path.repr coq_root in let convert_dirs (lp, cp) = try - let path = List.map convert_string (List.rev cp) @ prefix in + let path = List.rev_map convert_string cp @ prefix in Some (lp, Names.Dir_path.make path) with Exit -> None in -- cgit v1.2.3