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.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 3fce065613..6531036a1f 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -97,6 +97,7 @@ val pr_sort                : evar_map -> sorts -> std_ppcmds
 val pr_polymorphic         : bool -> std_ppcmds
 val pr_universe_instance   : evar_map -> Univ.universe_context -> std_ppcmds
 val pr_universe_ctx        : evar_map -> Univ.universe_context -> std_ppcmds
+val pr_universe_info_ind   : evar_map -> Univ.universe_info_ind -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
 
-- 
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.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 6531036a1f..9f4ea23b74 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -95,6 +95,7 @@ val pr_sort                : evar_map -> sorts -> std_ppcmds
 (** Universe constraints *)
 
 val pr_polymorphic         : bool -> std_ppcmds
+val pr_cumulative          : bool -> bool -> std_ppcmds
 val pr_universe_instance   : evar_map -> Univ.universe_context -> std_ppcmds
 val pr_universe_ctx        : evar_map -> Univ.universe_context -> std_ppcmds
 val pr_universe_info_ind   : evar_map -> Univ.universe_info_ind -> std_ppcmds
-- 
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.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 9f4ea23b74..f0a32bbbdf 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -98,7 +98,7 @@ val pr_polymorphic         : bool -> std_ppcmds
 val pr_cumulative          : bool -> bool -> std_ppcmds
 val pr_universe_instance   : evar_map -> Univ.universe_context -> std_ppcmds
 val pr_universe_ctx        : evar_map -> Univ.universe_context -> std_ppcmds
-val pr_universe_info_ind   : evar_map -> Univ.universe_info_ind -> std_ppcmds
+val pr_cumulativity_info   : evar_map -> Univ.cumulativity_info -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
 
-- 
cgit v1.2.3