aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/lib.ml2
1 files changed, 1 insertions, 1 deletions
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