diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/db | 2 | ||||
| -rw-r--r-- | dev/top_printers.ml | 8 |
2 files changed, 10 insertions, 0 deletions
@@ -44,3 +44,5 @@ install_printer Top_printers.prdelta install_printer Top_printers.ppfconstr install_printer Top_printers.ppgenarginfo install_printer Top_printers.ppist +install_printer Top_printers.ppconstrunderbindersidmap +install_printer Top_printers.ppunbound_ltac_var_map diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 0aa29cadf2..c0ef89a712 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -88,6 +88,14 @@ let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> (if id = id0 then mt () else spc () ++ str "<canonical: " ++ pr_id id ++ str ">")))) +let ppconstrunderbindersidmap l = ppidmap (fun id (l,c) -> + Id.print id ++ str "->" ++ hov 1 (str"[" ++ prlist Id.print l ++ str"]") + ++ str "," ++ spc () ++ Termops.print_constr c) + +let ppunbound_ltac_var_map l = ppidmap (fun id arg -> + Id.print id ++ str "->" ++ + str"<genarg:" ++ pr_argument_type(genarg_tag arg) ++ str">") + let pP s = pp (hov 0 s) let safe_pr_global = function |