From 57a0e3194660b68c972e084c7f80aa80979c4435 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 24 Apr 2008 11:17:47 +0000
Subject: - Add pretty-printers for Idpred, Cpred and transparent_state, used
 for   debugging and printing hint databases - Typeclasses unfold now
 correctly adds _global_ unfold hints. - New tactic autosimpl to do
 simplification using the declared unfold   hints in given hint databases. -
 Work on auto-modulo-some-delta (the declared Unfold constants),   actually
 used mostly if the goal contains evars, as Hint_db.map_auto   does not work
 up-to any conversions (yet). - Fix GenMul which was using the old semantics
 of failing early because   of variance checks, which is not possible in the
 new implementation. - Restrict when reflexive_morphism may be used using an
 extern tactic.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10842 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/base_include    | 3 +++
 dev/top_printers.ml | 4 ++++
 2 files changed, 7 insertions(+)

(limited to 'dev')

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)
-- 
cgit v1.2.3