From a5feb9687819c5e7ef0db6e7b74d0e236a296674 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 15 Sep 2017 21:01:57 +0200
Subject: Separate checking univ_decls and obtaining universe binder names.

---
 printing/printer.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index d7bb0460d5..4d5cfcba32 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -256,6 +256,13 @@ let safe_pr_constr t =
   let (sigma, env) = Pfedit.get_current_context () in
   safe_pr_constr_env env sigma t
 
+let pr_universe_ctx_set sigma c =
+  if !Detyping.print_universes && not (Univ.ContextSet.is_empty c) then
+    fnl()++pr_in_comment (fun c -> v 0
+      (Univ.pr_universe_context_set (Termops.pr_evd_level sigma) c)) c
+  else
+    mt()
+
 let pr_universe_ctx sigma c =
   if !Detyping.print_universes && not (Univ.UContext.is_empty c) then
     fnl()++pr_in_comment (fun c -> v 0 
-- 
cgit v1.2.3


From 58c0784745f8b2ba7523f246c4611d780c9f3f70 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 18 Sep 2017 14:50:07 +0200
Subject: When declaring constants/inductives use ContextSet if monomorphic.

Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.

There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
---
 printing/printer.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 4d5cfcba32..ae62920242 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -270,6 +270,10 @@ let pr_universe_ctx sigma c =
   else
     mt()
 
+let pr_constant_universes sigma = function
+  | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx
+  | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx
+
 let pr_cumulativity_info sigma cumi =
   if !Detyping.print_universes 
   && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
-- 
cgit v1.2.3