Little cleanup in auto.

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

2 files changed, 14 insertions, 8 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index a1550d8cb..ece948cff 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -138,6 +138,9 @@ module Hint_db = struct
     | Give_exact _ -> true
     | _ -> false
 
+  let rebuild_db st' db = 
+    { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map }
+
   let add_one (k,v) db =
     let st',rebuild =
       match v.code with
@@ -149,8 +152,8 @@ module Hint_db = struct
       | _ -> db.hintdb_state, false
     in
     let dnst, db = 
-      if db.use_dn then 
-	Some st', { db with hintdb_map = Constr_map.map (rebuild_dn st') db.hintdb_map }
+      if db.use_dn then
+	(Some st', if rebuild then rebuild_db st' db else db)
       else None, db
     in
     let oval = find k db in
@@ -164,11 +167,10 @@ module Hint_db = struct
     
   let transparent_state db = db.hintdb_state
 
-  let set_transparent_state db st = { db with hintdb_state = st }
-
-  let set_rigid db cst = 
-    let (ids,csts) = db.hintdb_state in
-      { db with hintdb_state = (ids, Cpred.remove cst csts) }
+  let set_transparent_state db st =
+    let db = if db.use_dn then rebuild_db st db else db in
+      { db with hintdb_state = st }
+	
 end
 
 module Hintdbmap = Gmap
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