aboutsummaryrefslogtreecommitdiff
path: root/dev/top_printers.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-05-14 14:10:09 +0200
committerGaëtan Gilbert2019-05-14 14:10:09 +0200
commit367df34f8a7ee619c0eb1c40cfa9d2bb432027ec (patch)
treec7da1a132b4091e8331c0534ecbada6ec13cfde0 /dev/top_printers.ml
parent9f11eeefc204bdad029b66f30bc6c52377af63ae (diff)
Add aucontext debug printer
Diffstat (limited to 'dev/top_printers.ml')
-rw-r--r--dev/top_printers.ml9
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 816316487c..90bb87d2ac 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -236,6 +236,15 @@ let ppnamedcontextval e =
let sigma = Evd.from_env env in
pp (pr_named_context env sigma (named_context_of_val 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)
+ | None -> prlev l
+ in
+ pp (pr_universe_context prlev (AUContext.repr auctx))
+
+
let ppenv e = pp
(str "[" ++ pr_named_context_of e Evd.empty ++ str "]" ++ spc() ++
str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]")