aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checker.ml2
-rw-r--r--checker/include2
-rw-r--r--dev/top_printers.ml4
-rw-r--r--interp/coqlib.ml2
-rw-r--r--kernel/nativecode.ml2
-rw-r--r--library/declare.ml2
-rw-r--r--library/library.ml2
-rw-r--r--parsing/egramcoq.ml2
-rw-r--r--plugins/extraction/table.ml2
-rw-r--r--plugins/firstorder/formula.ml2
-rw-r--r--plugins/funind/merge.ml4
-rw-r--r--plugins/xml/cic2acic.ml2
-rw-r--r--plugins/xml/xmlcommand.ml4
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/indrec.ml2
-rw-r--r--pretyping/recordops.ml2
-rw-r--r--printing/printer.ml2
-rw-r--r--tools/coqdep_common.ml2
-rw-r--r--toplevel/auto_ind_decl.ml2
-rw-r--r--toplevel/himsg.ml2
-rw-r--r--toplevel/mltop.ml2
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 04:14:21 +0000