From e9e8420df7a1799d9fcc86430c31a68820dc90c3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 22 Jun 2017 14:38:31 +0200
Subject: Add missing definition and fix #use include;; as suggested by
 @amintimany.

---
 dev/top_printers.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ff575e432c..1be72759c9 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -215,6 +215,7 @@ let ppuniverse_context_future c =
   let ctx = Future.force c in
     ppuniverse_context ctx
 let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
+let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   pp (pr_named_context (Global.env ()) Evd.empty (named_context_of_val e))
-- 
cgit v1.2.3