From 140f935ef271cbeb555a4a7e2015ee9a778ad394 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 Jul 2020 15:29:05 +0200
Subject: Fix debug printer for auctx in presence of Anonymous

---
 dev/top_printers.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f14edec639..34110f96cf 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -238,7 +238,9 @@ let ppnamedcontextval e =
 let ppaucontext auctx =
   let nas = AUContext.names auctx in
   let prlev l = match Level.var_index l with
-    | Some n -> Name.print nas.(n)
+    | Some n -> (match nas.(n) with
+        | Anonymous -> prlev l
+        | Name id -> Id.print id)
     | None -> prlev l
   in
   pp (pr_universe_context prlev (AUContext.repr auctx))
-- 
cgit v1.2.3