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/include | 2 --
 1 file changed, 2 deletions(-)

(limited to 'dev/include')

diff --git a/dev/include b/dev/include
index b982f4c9fa..c5de83b900 100644
--- a/dev/include
+++ b/dev/include
@@ -41,8 +41,6 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
-#install_printer  (* cumulativity info *) ppcumulativity_info;;
-#install_printer  (* abstract cumulativity info *) ppabstract_cumulativity_info;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;
-- 
cgit v1.2.3