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.

3 files changed, 17 insertions, 17 deletions

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