From c71e69a9be2094061e041d60614b090c8381f0b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:14:38 +0100 Subject: [api] Deprecate all legacy uses of Name.Id in core. This is a first step towards some of the solutions proposed in #6008. --- tactics/tacticals.mli | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'tactics/tacticals.mli') 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 -- cgit v1.2.3