From a9f0fd89cf3bb4b728eb451572a96f8599211380 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 30 Jan 2019 14:39:28 +0100
Subject: Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.
---
 dev/top_printers.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'dev/top_printers.mli')

diff --git a/dev/top_printers.mli b/dev/top_printers.mli
index 4d874cdd12..cb32d2294c 100644
--- a/dev/top_printers.mli
+++ b/dev/top_printers.mli
@@ -145,8 +145,6 @@ val ppevar_universe_context : UState.t -> unit
 val ppconstraints : Univ.Constraint.t -> unit
 val ppuniverseconstraints : UnivProblem.Set.t -> unit
 val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
-val ppcumulativity_info : Univ.CumulativityInfo.t -> unit
-val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit
 val ppuniverses : UGraph.t -> unit
 
 val ppnamedcontextval : Environ.named_context_val -> unit
-- 
cgit v1.2.3