From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Jun 2017 06:08:02 +0200
Subject: [proof] Deprecate redundant wrappers.

As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.

We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
---
 printing/printer.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 3c31dd96bf..d6f0778f75 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -17,7 +17,6 @@ open Nametab
 open Evd
 open Proof_type
 open Refiner
-open Pfedit
 open Constrextern
 open Ppconstr
 open Declarations
@@ -812,7 +811,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
   end
 
 let pr_nth_open_subgoal n =
-  let pf = get_pftreestate () in
+  let pf = Proof_global.give_me_the_proof () in
   let { it=gls ; sigma=sigma } = Proof.V82.subgoals pf in
   pr_subgoal n sigma gls
 
-- 
cgit v1.2.3


From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Sat, 1 Apr 2017 17:35:39 +0200
Subject: Using UInfoInd for universes in inductive types

It stores both universe constraints and subtyping information for
blocks of inductive declarations.

At this stage the there is no inference or checking implemented. The
subtyping information simply encodes equality of levels for the condition of
subtyping.
---
 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 d6f0778f75..c27a9b009d 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -261,6 +261,13 @@ let pr_universe_ctx sigma c =
   else
     mt()
 
+let pr_universe_info_ind sigma uii =
+  if !Detyping.print_universes && not (Univ.UInfoInd.is_empty uii) then
+    fnl()++pr_in_comment (fun uii -> v 0
+      (Univ.pr_universe_info_ind (Termops.pr_evd_level sigma) uii)) uii
+  else
+    mt()
+
 (**********************************************************************)
 (* Global references *)
 
-- 
cgit v1.2.3


From 0c94de1f8c598c1869f71fee86bdbe4f0000a502 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 4 May 2017 19:12:45 +0200
Subject: Add printing of cumulativity in inductive types

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

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index c27a9b009d..1d7b7cff0f 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -998,6 +998,11 @@ let pr_assumptionset env s =
 let xor a b = 
   (a && not b) || (not a && b)
 
+let pr_cumulative p b =
+  if p then
+    if b then str "Cumulative " else str "NonCumulative "
+  else str ""
+
 let pr_polymorphic b = 
   let print = xor (Flags.is_universe_polymorphism ()) b in
   if print then
-- 
cgit v1.2.3


From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 1 Jun 2017 16:18:19 +0200
Subject: Clean up universes of constants and inductives

---
 printing/printer.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index 1d7b7cff0f..3b0b6d5d23 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -261,10 +261,11 @@ let pr_universe_ctx sigma c =
   else
     mt()
 
-let pr_universe_info_ind sigma uii =
-  if !Detyping.print_universes && not (Univ.UInfoInd.is_empty uii) then
-    fnl()++pr_in_comment (fun uii -> v 0
-      (Univ.pr_universe_info_ind (Termops.pr_evd_level sigma) uii)) uii
+let pr_cumulativity_info sigma cumi =
+  if !Detyping.print_universes 
+  && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
+    fnl()++pr_in_comment (fun uii -> v 0 
+      (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi
   else
     mt()
 
@@ -998,10 +999,10 @@ let pr_assumptionset env s =
 let xor a b = 
   (a && not b) || (not a && b)
 
-let pr_cumulative p b =
-  if p then
-    if b then str "Cumulative " else str "NonCumulative "
-  else str ""
+let pr_cumulative poly cum =
+  if poly then
+    if cum then str "Cumulative " else str "NonCumulative "
+  else mt ()
 
 let pr_polymorphic b = 
   let print = xor (Flags.is_universe_polymorphism ()) b in
-- 
cgit v1.2.3