From ad8c2b7dab1b0759d1c304350523d6d2cc9c7b24 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 28 Dec 2020 22:02:22 +0100
Subject: Register a printer for fconstr substitutions in the kernel.

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

(limited to 'dev/top_printers.ml')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4faa12af79..6ce347ad59 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -85,6 +85,15 @@ let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
 let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
+let ppfsubst s =
+  let (s, k) = Esubst.Internal.repr s in
+  let sep () = str ";" ++ spc () in
+  let pr = function
+  | Esubst.Internal.REL n -> str "<#" ++ int n ++ str ">"
+  | Esubst.Internal.VAL (k, x) -> pr_constr (Vars.lift k (CClosure.term_of_fconstr x))
+  in
+  pp @@ str "[" ++ prlist_with_sep sep pr s ++ str "| " ++ int k ++ str "]"
+
 let ppnumtokunsigned n = pp (NumTok.Unsigned.print n)
 let ppnumtokunsignednat n = pp (NumTok.UnsignedNat.print n)
 
-- 
cgit v1.2.3