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