diff options
Diffstat (limited to 'dev/top_printers.ml')
| -rw-r--r-- | dev/top_printers.ml | 9 |
1 files changed, 9 insertions, 0 deletions
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) |