Backport PR #12628: Fix debug printer for auctx in presence of Anonymous

coq · Jul 15, 2020 · c948df5 · c948df5
2 parents bcb5a41 + c946925
commit c948df5
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
@@ -239,7 +239,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))