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 | ||||
| -rw-r--r-- | tactics/tactics.ml | 26 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 |
5 files changed, 14 insertions, 36 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) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 01351e2492..a42e4b44b5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -563,20 +563,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> end end -let warning_nameless_fix = - CWarnings.create ~name:"nameless-fix" ~category:"deprecated" Pp.(fun () -> - str "fix/cofix without a name are deprecated, please use the named version.") - -let fix ido n = match ido with - | None -> - warning_nameless_fix (); - Proofview.Goal.enter begin fun gl -> - let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id Id.Set.empty name gl in - mutual_fix id n [] 0 - end - | Some id -> - mutual_fix id n [] 0 +let fix id n = mutual_fix id n [] 0 let rec check_is_mutcoind env sigma cl = let b = whd_all env sigma cl in @@ -619,16 +606,7 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl -> end end -let cofix ido = match ido with - | None -> - warning_nameless_fix (); - Proofview.Goal.enter begin fun gl -> - let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id Id.Set.empty name gl in - mutual_cofix id [] 0 - end - | Some id -> - mutual_cofix id [] 0 +let cofix id = mutual_cofix id [] 0 (**************************************************************) (* Reduction and conversion tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 46f782eaa5..ddf78b1d4e 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -41,9 +41,9 @@ val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic val convert_hyp_no_check : named_declaration -> unit Proofview.tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic -val fix : Id.t option -> int -> unit Proofview.tactic +val fix : Id.t -> int -> unit Proofview.tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic -val cofix : Id.t option -> unit Proofview.tactic +val cofix : Id.t -> unit Proofview.tactic val convert : constr -> constr -> unit Proofview.tactic val convert_leq : constr -> constr -> unit Proofview.tactic |