5 files changed, 21 insertions, 11 deletions
diff --git a/lib/cArray.ml b/lib/cArray.ml
index 1591b0df2b..d08f24d490 100644
--- a/lib/cArray.ml
+++ b/lib/cArray.ml
@@ -287,8 +287,7 @@ let rev_of_list = function
   let () = set (len - 1) l in
   ans
 
-let map_to_list f v =
-  List.map f (Array.to_list v)
+let map_to_list = CList.map_of_array
 
 let map_of_list f l =
   let len = List.length l in
diff --git a/lib/cList.ml b/lib/cList.ml
index 0b93b901d5..ca69628af7 100644
--- a/lib/cList.ml
+++ b/lib/cList.ml
@@ -49,6 +49,7 @@ sig
     (int -> 'a -> bool) -> 'a list -> 'a list
   val partitioni :
     (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
+  val map_of_array : ('a -> 'b) -> 'a array -> 'b list
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
   val extend : bool list -> 'a -> 'a list -> 'a list
   val count : ('a -> bool) -> 'a list -> int
@@ -163,6 +164,21 @@ let map2 f l1 l2 = match l1, l2 with
   cast c
 | _ -> invalid_arg "List.map2"
 
+let rec map_of_array_loop f p a i l =
+  if Int.equal i l then ()
+  else
+    let c = { head = f (Array.unsafe_get a i); tail = [] } in
+    p.tail <- cast c;
+    map_of_array_loop f c a (i + 1) l
+
+let map_of_array f a =
+  let l = Array.length a in
+  if Int.equal l 0 then []
+  else
+    let c = { head = f (Array.unsafe_get a 0); tail = [] } in
+    map_of_array_loop f c a 1 l;
+    cast c
+
 let rec append_loop p tl = function
 | [] -> p.tail <- tl
 | x :: l ->
diff --git a/lib/cList.mli b/lib/cList.mli
index d280d060ac..8cb07da79c 100644
--- a/lib/cList.mli
+++ b/lib/cList.mli
@@ -53,7 +53,7 @@ sig
       [Invalid_argument "List.make"] if [n] is negative. *)
 
   val assign : 'a list -> int -> 'a -> 'a list
-  (** [assign l i x] set the [i]-th element of [l] to [x], starting from [0]. *)
+  (** [assign l i x] sets the [i]-th element of [l] to [x], starting from [0]. *)
 
   val distinct : 'a list -> bool
   (** Return [true] if all elements of the list are distinct. *)
@@ -91,6 +91,9 @@ sig
   val filteri : (int -> 'a -> bool) -> 'a list -> 'a list
   val partitioni : (int -> 'a -> bool) -> 'a list -> 'a list * 'a list
 
+  val map_of_array : ('a -> 'b) -> 'a array -> 'b list
+  (** [map_of_array f a] behaves as [List.map f (Array.to_list a)] *)
+
   val smartfilter : ('a -> bool) -> 'a list -> 'a list
   (** [smartfilter f [a1...an] = List.filter f [a1...an]] but if for all i
     [f ai = true], then [smartfilter f l == l] *)
diff --git a/lib/flags.ml b/lib/flags.ml
index 027ba16f0e..d4be81c61a 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -87,8 +87,6 @@ let in_toplevel = ref false
 
 let profile = false
 
-let xml_export = ref false
-
 let ide_slave = ref false
 let ideslave_coqtop_flags = ref None
 
@@ -96,7 +94,6 @@ let time = ref false
 
 let raw_print = ref false
 
-
 let univ_print = ref false
 
 let we_are_parsing = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 5af563b46e..3024c60396 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -56,11 +56,6 @@ val stm_debug : bool ref
 
 val profile : bool
 
-(* Legacy flags *)
-
-(* -xml option: xml hooks will be called *)
-val xml_export : bool ref
-
 (* -ide_slave: printing will be more verbose, will affect stm caching *)
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref