- 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

1 files changed, 16 insertions, 0 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 3e13e13927..521dad6a0d 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -244,6 +244,22 @@ let pr_restricted_named_context among env =
 	       pps)
           env ~init:(mt ()))
 
+
+let pr_predicate pr_elt (b, elts) = 
+  let pr_elts = prlist_with_sep spc pr_elt elts in
+    if b then
+      str"all" ++ 
+	(if elts = [] then mt () else str" except: " ++ pr_elts)
+    else
+      if elts = [] then str"none" else pr_elts
+      
+let pr_cpred p = pr_predicate pr_con (Cpred.elements p)
+let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p)
+
+let pr_transparent_state (ids, csts) = 
+  hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
+	str"CONSTANTS: " ++ pr_cpred csts ++ fnl ())
+
 let pr_subgoal_metas metas env=
   let pr_one (meta,typ) = 
     str "?" ++ int meta ++ str " : " ++