aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tacticals.mli16
-rw-r--r--tactics/tactics.ml2
-rw-r--r--tactics/tactics.mli6
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