From b02dc6b99aae142a497eaefd6ab1b0033ec3420f Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 16 Mar 2022 12:56:35 +0100
Subject: [PATCH] Properly deprecate ltn_leq_trans
Deprecation only works for notations, it is a noop on definitions.
There is now a warning in Coq, https://github.com/coq/coq/pull/15760
to avoid this in future releases.
---
util/nat.v | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/util/nat.v b/util/nat.v
index 3a02c22c1..0fd58b4b8 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -127,6 +127,7 @@ End Interval.
Nonetheless we introduce it here because an additional (even though
arguably redundant) lemma doesn't hurt, and for newcomers the apparent
absence of the mirror case of [leq_ltn_trans] can be somewhat confusing. *)
-#[deprecated(since="0.4",note="Use leq_trans instead since n < m is just a notation for n.+1 <= m (c.f., comment in util/nat.v).")]
-Lemma ltn_leq_trans [n m p] : m < n -> n <= p -> m < p.
+Lemma ltn_leq_trans_deprecated [n m p] : m < n -> n <= p -> m < p.
Proof. exact: leq_trans. Qed.
+#[deprecated(since="0.4",note="Use leq_trans instead since n < m is just a notation for n.+1 <= m (c.f., comment in util/nat.v).")]
+Notation ltn_leq_trans := ltn_leq_trans_deprecated.
--
GitLab