diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 3 | ||||
| -rw-r--r-- | dev/top_printers.ml | 4 |
2 files changed, 7 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include index d3301c88bd..255e28a668 100644 --- a/dev/base_include +++ b/dev/base_include @@ -32,6 +32,9 @@ #install_printer (* constr *) print_pure_constr;; #install_printer (* patch *) ppripos;; #install_printer (* values *) ppvalues;; +#install_printer (* Idpred.t *) pp_idpred;; +#install_printer (* Cpred.t *) pp_cpred;; +#install_printer (* transparent_state *) pp_transparent_state;; #install_printer ppzipper;; #install_printer ppstack;; #install_printer ppatom;; diff --git a/dev/top_printers.ml b/dev/top_printers.ml index c67307d36f..a63c6c2dd6 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -93,6 +93,10 @@ let ppj j = pp (genppj pr_ljudge j) let prsubst s = pp (Mod_subst.debug_pr_subst s) +let pp_idpred s = pp (pr_idpred s) +let pp_cpred s = pp (pr_cpred s) +let pp_transparent_state s = pp (pr_transparent_state s) + (* proof printers *) let ppmetas metas = pp(pr_metaset metas) let ppevm evd = pp(pr_evar_map evd) |