From 15b1856edd593b39d63d23584a4f5acec0eeb592 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Thu, 15 Jun 2017 16:50:05 +0200
Subject: Fix a bug in cumulativity

---
 dev/include | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'dev/include')

diff --git a/dev/include b/dev/include
index 1d87456de7..31ae5da71a 100644
--- a/dev/include
+++ b/dev/include
@@ -41,7 +41,8 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
-#install_printer  (* univ info *) ppcumulativity_info;;
+#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