Adding genarg printer to debugger.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16594 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 10 insertions, 0 deletions

diff --git a/dev/db b/dev/db
index e7346c6b49..10926be086 100644
--- a/dev/db
+++ b/dev/db
@@ -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                                    *)