Little cleanup in auto.

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

1 files changed, 5 insertions, 1 deletions

diff --git a/tactics/auto.mli b/tactics/auto.mli
index 27ecca983..95e6ef3b2 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -57,7 +57,6 @@ module Hint_db :
 
     val transparent_state : t -> transparent_state
     val set_transparent_state : t -> transparent_state -> t
-    val set_rigid : t -> constant -> t
   end
 
 type hint_db_name = string
@@ -68,6 +67,11 @@ val searchtable_map : hint_db_name -> hint_db
 
 val searchtable_add : (hint_db_name * hint_db) -> unit
 
+(* [create_hint_db local name st use_dn]. 
+   [st] is a transparency state for unification using this db
+   [use_dn] switches the use of the discrimination net for all hints 
+   and patterns. *)
+
 val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit
 
 val current_db_names : unit -> hint_db_name list