diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/db | 1 | ||||
| -rw-r--r-- | dev/top_printers.ml | 9 |
2 files changed, 10 insertions, 0 deletions
@@ -38,3 +38,4 @@ install_printer Top_printers.pploc install_printer Top_printers.prsubst install_printer Top_printers.prdelta install_printer Top_printers.ppfconstr +install_printer Top_printers.ppgenarginfo diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 939e9422ac..f59c300a9e 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -379,6 +379,15 @@ let pp_argument_type t = pp (pr_argument_type t) let pp_generic_argument arg = pp(str"<genarg:"++pr_argument_type(genarg_tag arg)++str">") +let ppgenarginfo arg = + let tpe = pr_argument_type (genarg_tag arg) in + let pr_gtac _ x = Pptactic.pr_glob_tactic (Global.env()) x in + try + let data = Pptactic.pr_top_generic pr_constr pr_lconstr pr_gtac pr_constr_pattern arg in + pp (str "<genarg:" ++ tpe ++ str " := [ " ++ data ++ str " ] >") + with _any -> + pp (str "<genarg:" ++ tpe ++ str ">") + (**********************************************************************) (* Vernac-level debugging commands *) |