Better use of transparency information for local hypotheses:

- make hyps rigid in the dnet if they're not let-ins
- use existing typeclass-related transparency information for the new
hints.
Make the dnet better by indexing products, lambdas and sorts too.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12350 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 0 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index 007a116d1..1910bd139 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -104,6 +104,8 @@ val print_hint_ref : global_reference -> unit
 
 val print_hint_db_by_name : hint_db_name -> unit
 
+val print_hint_db : Hint_db.t -> unit
+
 (* [make_exact_entry pri (c, ctyp)].
    [c] is the term given as an exact proof to solve the goal;
    [ctyp] is the type of [c]. *)