From b0ef649660542ae840ea945d7ab4f1f3ae7b85cd Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 28 Apr 2018 17:58:08 +0200
Subject: Split off Universes functions dealing with names.

This API is a bit strange, I expect it will change at some point.
---
 printing/printmod.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing/printmod.ml')

diff --git a/printing/printmod.ml b/printing/printmod.ml
index e076c10f3b..3c805b327d 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -140,7 +140,7 @@ let print_mutual_inductive env mind mib udecl =
                        (AUContext.instance (Declareops.inductive_polymorphic_context mib)))
     else []
   in
-  let bl = Universes.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
+  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++
          Printer.pr_cumulative
@@ -183,7 +183,7 @@ let print_record env mind mib udecl =
   let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
   let fields = get_fields cstrtype in
   let envpar = push_rel_context params env in
-  let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
+  let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0))
       (Array.to_list (Univ.Instance.to_array u)) udecl in
   let sigma = Evd.from_ctx (UState.of_binders bl) in
   let keyword =
-- 
cgit v1.2.3