- 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

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)