diff options
| -rw-r--r-- | tactics/btermdn.ml | 2 | ||||
| -rw-r--r-- | tactics/btermdn.mli | 2 | ||||
| -rw-r--r-- | tactics/dn.ml | 2 | ||||
| -rw-r--r-- | tactics/dn.mli | 2 | ||||
| -rw-r--r-- | tactics/hints.ml | 16 |
5 files changed, 13 insertions, 11 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 1f5177c3d..b87d65753 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -144,7 +144,7 @@ struct type t = Dn.t - let create = Dn.create + let empty = Dn.empty let add = function | None -> diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 6c396b4c8..f29d18615 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -28,7 +28,7 @@ module Make : sig type t - val create : unit -> t + val empty : t val add : transparent_state option -> t -> (constr_pattern * Z.t) -> t val rmv : transparent_state option -> t -> (constr_pattern * Z.t) -> t diff --git a/tactics/dn.ml b/tactics/dn.ml index 3b1614d6c..aed2c2832 100644 --- a/tactics/dn.ml +++ b/tactics/dn.ml @@ -38,7 +38,7 @@ struct type t = Trie.t - let create () = Trie.empty + let empty = Trie.empty (* [path_of dna pat] returns the list of nodes of the pattern [pat] read in prefix ordering, [dna] is the function returning the main node of a pattern *) diff --git a/tactics/dn.mli b/tactics/dn.mli index 20407e9d9..2a60c3eb8 100644 --- a/tactics/dn.mli +++ b/tactics/dn.mli @@ -10,7 +10,7 @@ sig type t - val create : unit -> t + val empty : t (** [add t f (tree,inf)] adds a structured object [tree] together with the associated information [inf] to the table [t]; the function diff --git a/tactics/hints.ml b/tactics/hints.ml index dea47794e..55d62e151 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -171,7 +171,7 @@ type search_entry = { let empty_se = { sentry_nopat = []; sentry_pat = []; - sentry_bnet = Bounded_net.create (); + sentry_bnet = Bounded_net.empty; sentry_mode = []; } @@ -206,7 +206,7 @@ let rebuild_dn st se = let dn' = List.fold_left (fun dn (id, t) -> Bounded_net.add (Some st) dn (Option.get t.pat, (id, t))) - (Bounded_net.create ()) se.sentry_pat + Bounded_net.empty se.sentry_pat in { se with sentry_bnet = dn' } @@ -394,7 +394,7 @@ module Hint_db = struct hintdb_state : Names.transparent_state; hintdb_cut : hints_path; hintdb_unfolds : Id.Set.t * Cset.t; - mutable hintdb_max_id : int; + hintdb_max_id : int; use_dn : bool; hintdb_map : search_entry Constr_map.t; (* A list of unindexed entries starting with an unfoldable constant @@ -402,8 +402,9 @@ module Hint_db = struct hintdb_nopat : (global_reference option * stored_data) list } - let next_hint_id t = - let h = t.hintdb_max_id in t.hintdb_max_id <- succ t.hintdb_max_id; h + let next_hint_id db = + let h = db.hintdb_max_id in + { db with hintdb_max_id = succ db.hintdb_max_id }, h let empty st use_dn = { hintdb_state = st; hintdb_cut = PathEmpty; @@ -510,8 +511,9 @@ module Hint_db = struct state, { db with hintdb_unfolds = unfs }, true | _ -> db.hintdb_state, db, false in - let db = if db.use_dn && rebuild then rebuild_db st' db else db - in addkv k (next_hint_id db) v db + let db = if db.use_dn && rebuild then rebuild_db st' db else db in + let db, id = next_hint_id db in + addkv k id v db let add_list l db = List.fold_left (fun db k -> add_one k db) db l |