diff options
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index ecc0930c1..7ac79356f 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -152,7 +152,7 @@ let lookup_tacs (hdc,c) st (l,l',dn) = module Constr_map = Map.Make(RefOrdered) let is_transparent_gr (ids, csts) = function - | VarRef id -> Idpred.mem id ids + | VarRef id -> Id.Pred.mem id ids | ConstRef cst -> Cpred.mem cst csts | IndRef _ | ConstructRef _ -> false @@ -308,7 +308,7 @@ module Hint_db = struct type t = { hintdb_state : Names.transparent_state; hintdb_cut : hints_path; - hintdb_unfolds : Idset.t * Cset.t; + hintdb_unfolds : Id.Set.t * Cset.t; mutable hintdb_max_id : int; use_dn : bool; hintdb_map : search_entry Constr_map.t; @@ -322,7 +322,7 @@ module Hint_db = struct let empty st use_dn = { hintdb_state = st; hintdb_cut = PathEmpty; - hintdb_unfolds = (Idset.empty, Cset.empty); + hintdb_unfolds = (Id.Set.empty, Cset.empty); hintdb_max_id = 0; use_dn = use_dn; hintdb_map = Constr_map.empty; @@ -384,7 +384,7 @@ module Hint_db = struct | Unfold_nth egr -> let addunf (ids,csts) (ids',csts') = match egr with - | EvalVarRef id -> (Idpred.add id ids, csts), (Idset.add id ids', csts') + | EvalVarRef id -> (Id.Pred.add id ids, csts), (Id.Set.add id ids', csts') | EvalConstRef cst -> (ids, Cpred.add cst csts), (ids', Cset.add cst csts') in let state, unfs = addunf db.hintdb_state db.hintdb_unfolds in @@ -611,7 +611,7 @@ let add_transparency dbname grs b = List.fold_left (fun (ids, csts) gr -> match gr with | EvalConstRef c -> (ids, (if b then Cpred.add else Cpred.remove) c csts) - | EvalVarRef v -> (if b then Idpred.add else Idpred.remove) v ids, csts) + | EvalVarRef v -> (if b then Id.Pred.add else Id.Pred.remove) v ids, csts) st grs in searchtable_add (dbname, Hint_db.set_transparent_state db st') @@ -806,7 +806,7 @@ type hints_entry = | HintsExternEntry of int * (patvar list * constr_pattern) option * glob_tactic_expr -let h = id_of_string "H" +let h = Id.of_string "H" exception Found of constr * types @@ -833,8 +833,8 @@ let prepare_hint env (sigma,c) = let rec iter c = try find_next_evar c; c with Found (evar,t) -> - let id = next_ident_away_from h (fun id -> Idset.mem id !vars) in - vars := Idset.add id !vars; + let id = next_ident_away_from h (fun id -> Id.Set.mem id !vars) in + vars := Id.Set.add id !vars; subst := (evar,mkVar id)::!subst; mkNamedLambda id t (iter (replace_term evar (mkVar id) c)) in iter c @@ -1312,7 +1312,7 @@ and my_find_search_delta db_list local_db hdc concl = let l = match hdc with None -> Hint_db.map_none db | Some hdc -> - if (Idpred.is_empty ids && Cpred.is_empty csts) + if (Id.Pred.is_empty ids && Cpred.is_empty csts) then Hint_db.map_auto (hdc,concl) db else Hint_db.map_all hdc db in {flags with modulo_delta = st}, l |