From ad7eeccceb1c75972a98b30328049c458e2dbab4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 Feb 2020 21:17:05 +0100
Subject: [PATCH] Mark `iAlways` as deprecated in the code.
It was already marked as deprecated in `doc/proof_mode.md`.
---
theories/proofmode/ltac_tactics.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 75d192389..e01b36782 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1341,6 +1341,8 @@ Tactic Notation "iModIntro" uconstr(sel) :=
|pm_prettify (* reduce redexes created by instantiation *)
(* subgoal *) ].
Tactic Notation "iModIntro" := iModIntro _.
+
+(** DEPRECATED *)
Tactic Notation "iAlways" := iModIntro.
(** * Later *)
--
GitLab