diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 16 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.mli | 6 |
5 files changed, 14 insertions, 14 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2b5bbfcd1..9097aebd0 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -439,7 +439,7 @@ let autounfolds db occs cls gl = in let (ids, csts) = Hint_db.unfolds db in let hyps = pf_ids_of_hyps gl in - let ids = Idset.filter (fun id -> List.mem id hyps) ids in + let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) in Proofview.V82.of_tactic (unfold_option unfolds cls) gl diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bce0dda10..07eea7b63 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -623,7 +623,7 @@ module New = struct let name_elim = match EConstr.kind sigma elim with | Const (kn, _) -> string_of_con kn - | Var id -> string_of_id id + | Var id -> Id.to_string id | _ -> "\b" in user_err ~hdr:"Tacticals.general_elim_then_using" diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 2a04c413b..3abd42d46 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -226,12 +226,12 @@ module New : sig val nLastDecls : 'a Proofview.Goal.t -> int -> named_context - val ifOnHyp : (identifier * types -> bool) -> - (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> - identifier -> unit Proofview.tactic + val ifOnHyp : (Id.t * types -> bool) -> + (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) -> + Id.t -> unit Proofview.tactic - val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic - val onLastHypId : (identifier -> unit tactic) -> unit tactic + val onNthHypId : int -> (Id.t -> unit tactic) -> unit tactic + val onLastHypId : (Id.t -> unit tactic) -> unit tactic val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic @@ -239,9 +239,9 @@ module New : sig (named_context -> unit tactic) -> unit tactic val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic - val tryAllHyps : (identifier -> unit tactic) -> unit tactic - val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic - val onClause : (identifier option -> unit tactic) -> clause -> unit tactic + val tryAllHyps : (Id.t -> unit tactic) -> unit tactic + val tryAllHypsAndConcl : (Id.t option -> unit tactic) -> unit tactic + val onClause : (Id.t option -> unit tactic) -> clause -> unit tactic val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> sorts_family diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f8f9e029b..6f67606d2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1376,7 +1376,7 @@ let enforce_prop_bound_names rename tac = (* "very_standard" says that we should have "H" names only, but this would break compatibility even more... *) let s = match Namegen.head_name sigma t with - | Some id when not very_standard -> string_of_id id + | Some id when not very_standard -> Id.to_string id | _ -> "" in Name (add_suffix Namegen.default_prop_ident s) else diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 32923ea81..98cf1b437 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -271,7 +271,7 @@ type eliminator = { val general_elim : evars_flag -> clear_flag -> constr with_bindings -> eliminator -> unit Proofview.tactic -val general_elim_clause : evars_flag -> unify_flags -> identifier option -> +val general_elim_clause : evars_flag -> unify_flags -> Id.t option -> clausenv -> eliminator -> unit Proofview.tactic val default_elim : evars_flag -> clear_flag -> constr with_bindings -> @@ -355,7 +355,7 @@ val assert_before : Name.t -> types -> unit Proofview.tactic val assert_after : Name.t -> types -> unit Proofview.tactic val assert_as : (* true = before *) bool -> - (* optionally tell if a specialization of some hyp: *) identifier option -> + (* optionally tell if a specialization of some hyp: *) Id.t option -> intro_pattern option -> constr -> unit Proofview.tactic (** Implements the tactics assert, enough and pose proof; note that "by" @@ -428,7 +428,7 @@ module Simple : sig val eapply : constr -> unit Proofview.tactic val elim : constr -> unit Proofview.tactic val case : constr -> unit Proofview.tactic - val apply_in : identifier -> constr -> unit Proofview.tactic + val apply_in : Id.t -> constr -> unit Proofview.tactic end |