Skip to content

Commit 6cba73d

Browse files
committed
update since field in deprecation
Signed-off-by: Ali Caglayan <[email protected]>
1 parent 0dca53c commit 6cba73d

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

theories/Basics/Tactics.v

+2-2
Original file line numberDiff line numberDiff line change
@@ -326,7 +326,7 @@ Tactic Notation "napply'" uconstr(term)
326326

327327
(** TODO: remove when min Coq/Rocq version is 9.1 (~ end of 2026). *)
328328
#[deprecated(note="nrapply was renamed to napply and will be removed soon",
329-
since="Coq-HoTT v9.1")]
329+
since="2025-03-11")]
330330
Tactic Notation "nrapply" uconstr(term) := napply term.
331331

332332
(** [rapply] is equivalent in strength to [napply], i.e., it should succeed iff [napply] succeeds, but it solves all possible typeclasses after successful unification with the goal. The implementation is: try [nrefine t, t _, t _ _], ... until success; upon success, revert the last (successful) application of [nrefine] and call [refine (t _ _ _)]. *)
@@ -350,7 +350,7 @@ Tactic Notation "snapply'" uconstr(term)
350350

351351
(** TODO: remove when min Coq/Rocq version is 9.1 (~ end of 2026). *)
352352
#[deprecated(note="snrapply was renamed to snapply and will be removed soon",
353-
since="Coq-HoTT v9.1")]
353+
since="2025-03-11")]
354354
Tactic Notation "snrapply" uconstr(term) := snapply term.
355355

356356
(** See comment for [rapply]. This cannot be simplified to [snrefine x] because we don't want the [global_axiom] tactic to run here. *)

0 commit comments

Comments
 (0)