From 23ef45aa14308aa0b1e1b1f6061ec9e7e7634e49 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 1 Oct 2018 13:40:45 +0200
Subject: 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.
---
 library/lib.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

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
-- 
cgit v1.2.3