diff options
| -rw-r--r-- | tactics/auto.ml | 16 | ||||
| -rw-r--r-- | tactics/auto.mli | 6 |
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 |