diff options
author | 2013-06-19 19:42:40 +0000 | |
---|---|---|
committer | 2013-06-19 19:42:40 +0000 | |
commit | 902d8031333704b8c1f4b73aa72b1a015530f3a4 (patch) | |
tree | dd4e6c06cd2bf0a018d3d1af45f64f5b94ba019b /dev/top_printers.ml | |
parent | f68ff500a9090da58f573ce68e4b8b080e871e28 (diff) |
Adding genarg printer to debugger.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16594 85f007b7-540e-0410-9357-904b9bb8a0f7
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 939e9422a..f59c300a9 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 *) |