diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/autorewrite.ml | 2 | ||||
| -rw-r--r-- | tactics/hints.ml | 16 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 2 |
3 files changed, 10 insertions, 10 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 627ac31f50..0b0e629ab5 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -30,7 +30,7 @@ let subst_hint subst hint = let cst' = subst_mps subst hint.rew_lemma in let typ' = subst_mps subst hint.rew_type in let pat' = subst_mps subst hint.rew_pat in - let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in + let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else { hint with rew_lemma = cst'; rew_type = typ'; diff --git a/tactics/hints.ml b/tactics/hints.ml index 39034a19b4..3ade5314b9 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -448,7 +448,7 @@ let subst_path_atom subst p = | PathAny -> p | PathHints grs -> let gr' gr = fst (subst_global subst gr) in - let grs' = List.smartmap gr' grs in + let grs' = List.Smart.map gr' grs in if grs' == grs then p else PathHints grs' let rec subst_hints_path subst hp = @@ -654,7 +654,7 @@ struct let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l - let remove_sdl p sdl = List.smartfilter p sdl + let remove_sdl p sdl = List.Smart.filter p sdl let remove_he st p se = let sl1' = remove_sdl p se.sentry_nopat in @@ -666,7 +666,7 @@ struct let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in - let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in + let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } let remove_one gr db = remove_list [gr] db @@ -1065,8 +1065,8 @@ let subst_autohint (subst, obj) = in if gr' == gr then gr else gr' in let subst_hint (k,data as hint) = - let k' = Option.smartmap subst_key k in - let pat' = Option.smartmap (subst_pattern subst) data.pat in + let k' = Option.Smart.map subst_key k in + let pat' = Option.Smart.map (subst_pattern subst) data.pat in let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in let code' = match data.code.obj with | Res_pf (c,t,ctx) -> @@ -1104,13 +1104,13 @@ let subst_autohint (subst, obj) = let action = match obj.hint_action with | CreateDB _ -> obj.hint_action | AddTransparency (grs, b) -> - let grs' = List.smartmap (subst_evaluable_reference subst) grs in + let grs' = List.Smart.map (subst_evaluable_reference subst) grs in if grs == grs' then obj.hint_action else AddTransparency (grs', b) | AddHints hintlist -> - let hintlist' = List.smartmap subst_hint hintlist in + let hintlist' = List.Smart.map subst_hint hintlist in if hintlist' == hintlist then obj.hint_action else AddHints hintlist' | RemoveHints grs -> - let grs' = List.smartmap (subst_global_reference subst) grs in + let grs' = List.Smart.map (subst_global_reference subst) grs in if grs == grs' then obj.hint_action else RemoveHints grs' | AddCut path -> let path' = subst_hints_path subst path in diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 6d0da0dfaa..21520f5d2b 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -53,7 +53,7 @@ let subst_one_scheme subst (ind,const) = (subst_ind subst ind,subst_constant subst const) let subst_scheme (subst,(kind,l)) = - (kind,Array.map (subst_one_scheme subst) l) + (kind,Array.Smart.map (subst_one_scheme subst) l) let discharge_scheme (_,(kind,l)) = Some (kind,Array.map (fun (ind,const) -> |