Use arrays of names instead of lists in abstract universe names.

There is little point in having a list, as there is virtually no sharing
nor expansion of bound universe names. This representation is thus more
compact.

9 files changed, 26 insertions, 25 deletions

diff --git a/checker/values.ml b/checker/values.ml
index 68bac10839..e21acd8179 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -122,7 +122,7 @@ let v_cstrs =
 let v_variance = v_enum "variance" 3
 
 let v_instance = Annot ("instance", Array v_level)
-let v_abs_context = v_tuple "abstract_universe_context" [|List v_name; v_cstrs|]
+let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|]
 let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
diff --git a/engine/univNames.ml b/engine/univNames.ml
index b7ccd2372f..ad91d31f87 100644
--- a/engine/univNames.ml
+++ b/engine/univNames.ml
@@ -36,9 +36,9 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 let empty_binders = Id.Map.empty
 
-let universe_binders_of_global ref : Name.t list =
+let universe_binders_of_global ref : Name.t array =
   try AUContext.names (Environ.universes_of_global (Global.env ()) ref)
-  with Not_found -> []
+  with Not_found -> [||]
 
 let name_universe lvl =
   (** Best-effort naming from the string representation of the level. This is
@@ -51,12 +51,13 @@ let compute_instance_binders inst ubinders =
     try Name (LMap.find lvl revmap)
     with Not_found -> Name (name_universe lvl)
   in
-  Array.map_to_list map (Instance.to_array inst)
+  Array.map map (Instance.to_array inst)
 
 type univ_name_list = Names.lname list
 
 let universe_binders_with_opt_names ref names =
   let orig = universe_binders_of_global ref in
+  let orig = Array.to_list orig in
   let udecl = match names with
   | None -> orig
   | Some udecl ->
diff --git a/engine/univNames.mli b/engine/univNames.mli
index b00c5fda95..dc669f45d6 100644
--- a/engine/univNames.mli
+++ b/engine/univNames.mli
@@ -19,7 +19,7 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 val empty_binders : universe_binders
 
-val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t list
+val compute_instance_binders : Instance.t -> universe_binders -> Names.Name.t array
 
 type univ_name_list = Names.lname list
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 87fa385a60..58bb782f15 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -30,8 +30,8 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 
 type inductive_universes =
   | Monomorphic_ind_entry of Univ.ContextSet.t
-  | Polymorphic_ind_entry of Name.t list * Univ.UContext.t
-  | Cumulative_ind_entry of Name.t list * Univ.CumulativityInfo.t
+  | Polymorphic_ind_entry of Name.t array * Univ.UContext.t
+  | Cumulative_ind_entry of Name.t array * Univ.CumulativityInfo.t
 
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
@@ -60,7 +60,7 @@ type 'a const_entry_body = 'a proof_output Future.computation
 
 type constant_universes_entry =
   | Monomorphic_const_entry of Univ.ContextSet.t
-  | Polymorphic_const_entry of Name.t list * Univ.UContext.t
+  | Polymorphic_const_entry of Name.t array * Univ.UContext.t
 
 type 'a in_constant_universes_entry = 'a * constant_universes_entry
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index ec6dcee834..0edf750997 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -937,29 +937,29 @@ let hcons_universe_context = UContext.hcons
 
 module AUContext =
 struct
-  type t = Names.Name.t list constrained
+  type t = Names.Name.t array constrained
 
   let repr (inst, cst) =
-    (Array.init (List.length inst) (fun i -> Level.var i), cst)
+    (Array.init (Array.length inst) (fun i -> Level.var i), cst)
 
   let pr f ?variance ctx = UContext.pr f ?variance (repr ctx)
 
   let instantiate inst (u, cst) =
-    assert (List.length u = Array.length inst);
+    assert (Array.length u = Array.length inst);
     subst_instance_constraints inst cst
 
   let names (nas, _) = nas
 
   let hcons (univs, cst) =
-    (List.map Names.Name.hcons univs, hcons_constraints cst)
+    (Array.map Names.Name.hcons univs, hcons_constraints cst)
 
-  let empty = ([], Constraint.empty)
+  let empty = ([||], Constraint.empty)
 
-  let is_empty (nas, cst) = List.is_empty nas && Constraint.is_empty cst
+  let is_empty (nas, cst) = Array.is_empty nas && Constraint.is_empty cst
 
-  let union (nas, cst) (nas', cst') = (nas @ nas', Constraint.union cst cst')
+  let union (nas, cst) (nas', cst') = (Array.append nas nas', Constraint.union cst cst')
 
-  let size (nas, _) = List.length nas
+  let size (nas, _) = Array.length nas
 
 end
 
@@ -1173,16 +1173,16 @@ let make_inverse_instance_subst i =
       LMap.empty arr
 
 let make_abstract_instance (ctx, _) = 
-  Array.init (List.length ctx) (fun i -> Level.var i)
+  Array.init (Array.length ctx) (fun i -> Level.var i)
 
 let abstract_universes nas ctx =
   let instance = UContext.instance ctx in
-  let () = assert (Int.equal (List.length nas) (Instance.length instance)) in
+  let () = assert (Int.equal (Array.length nas) (Instance.length instance)) in
   let subst = make_instance_subst instance in
   let cstrs = subst_univs_level_constraints subst 
       (UContext.constraints ctx)
   in
-  let ctx = UContext.make (nas, cstrs) in
+  let ctx = (nas, cstrs) in
   instance, ctx
 
 let abstract_cumulativity_info nas (univs, variance) =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 3788d8f90d..de7b334ae4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -344,7 +344,7 @@ sig
   val instantiate : Instance.t -> t -> Constraint.t
   (** Generate the set of instantiated Constraint.t **)
 
-  val names : t -> Names.Name.t list
+  val names : t -> Names.Name.t array
   (** Return the names of the bound universe variables *)
 
 end
@@ -466,8 +466,8 @@ val make_instance_subst : Instance.t -> universe_level_subst
 
 val make_inverse_instance_subst : Instance.t -> universe_level_subst
 
-val abstract_universes : Names.Name.t list -> UContext.t -> Instance.t * AUContext.t
-val abstract_cumulativity_info : Names.Name.t list -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
+val abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t
+val abstract_cumulativity_info : Names.Name.t array -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
 (** TODO: move universe abstraction out of the kernel *)
 
 val make_abstract_instance : AUContext.t -> Instance.t
diff --git a/library/lib.ml b/library/lib.ml
index ccf3b4d068..9c13cdafdb 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -495,7 +495,7 @@ let name_instance inst =
             See univNames.ml for a similar hack. *)
         Name (Id.of_string_soft (Univ.Level.to_string lvl))
   in
-  Array.map_to_list map (Univ.Instance.to_array inst)
+  Array.map map (Univ.Instance.to_array inst)
 
 let add_section_replacement f g poly hyps =
   match !sectab with
diff --git a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
index c4b36fb9e0..047f4cd080 100644
--- a/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
+++ b/test-suite/misc/poly-capture-global-univs/src/evilImpl.ml
@@ -15,7 +15,7 @@ let evil t f =
   let tc = mkConst tc in
 
   let fe = Declare.definition_entry
-      ~univs:(Polymorphic_const_entry ([Anonymous], UContext.make (Instance.of_array [|u|],Constraint.empty)))
+      ~univs:(Polymorphic_const_entry ([|Anonymous|], UContext.make (Instance.of_array [|u|],Constraint.empty)))
       ~types:(Term.mkArrow tc tu)
       (mkLambda (Name.Name (Id.of_string "x"), tc, mkRel 1))
   in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3bac4a6555..476db06c54 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -380,7 +380,7 @@ let context poly l =
         begin
           let uctx = Evd.universe_context_set sigma in
           Declare.declare_universe_context poly uctx;
-          if poly then Polymorphic_const_entry ([], Univ.UContext.empty)
+          if poly then Polymorphic_const_entry ([||], Univ.UContext.empty)
           else Monomorphic_const_entry Univ.ContextSet.empty
         end
       else if poly then