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 +++
 1 file changed, 3 insertions(+)

(limited to 'dev/base_include')

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