From 9ddd30f8edfef4bde13716a0f1407c5a6468fb42 Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Tue, 28 Nov 2023 16:57:05 +0100 Subject: [PATCH] Deprecate obsolete files in NArith TODO: look at Ndec.v --- theories/NArith/Ndec.v | 1 + theories/NArith/Ndigits.v | 1 + theories/NArith/Ndist.v | 2 ++ theories/NArith/Ndiv_def.v | 1 + theories/NArith/Ngcd_def.v | 1 + theories/NArith/Nsqrt_def.v | 1 + 6 files changed, 7 insertions(+) diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index e246988778a2..887d853f16b6 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -19,6 +19,7 @@ Require Import Ndigits. Local Open Scope N_scope. +Attributes deprecated(since="8.19", note="TODO"). (** Obsolete results about boolean comparisons over [N], kept for compatibility with IntMap and SMC. *) diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index 0b310ba9350b..65409d421259 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -14,6 +14,7 @@ Require Import Bool Morphisms Setoid Bvector BinPos BinNat PeanoNat Pnat Nnat Local Open Scope N_scope. Local Open Scope program_scope. +Attributes deprecated(since="8.19", note="Use NArith.BinNat instead."). (** This file is mostly obsolete, see directly [BinNat] now. *) Local Set Warnings "-deprecated". diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v index 3a92395ac236..c3cd84af6ae3 100644 --- a/theories/NArith/Ndist.v +++ b/theories/NArith/Ndist.v @@ -12,6 +12,8 @@ Require Import BinPos. Require Import BinNat. Require Import Ndigits. +Attributes deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it."). + Local Set Warnings "-deprecated". (** An ultrametric distance over [N] numbers *) diff --git a/theories/NArith/Ndiv_def.v b/theories/NArith/Ndiv_def.v index 7614e2beffd8..81ef9fe38243 100644 --- a/theories/NArith/Ndiv_def.v +++ b/theories/NArith/Ndiv_def.v @@ -11,6 +11,7 @@ Require Import BinNat. Local Open Scope N_scope. +Attributes deprecated(since="8.19", note="Use NArith.BinNat instead."). (** Obsolete file, see [BinNat] now, only compatibility notations remain here. *) diff --git a/theories/NArith/Ngcd_def.v b/theories/NArith/Ngcd_def.v index baac5e9d4c93..893fb14c31cf 100644 --- a/theories/NArith/Ngcd_def.v +++ b/theories/NArith/Ngcd_def.v @@ -11,6 +11,7 @@ Require Import BinPos BinNat. Local Open Scope N_scope. +Attributes deprecated(since="8.19", note="Require BinNat instead."). (** Obsolete file, see [BinNat] now, only compatibility notations remain here. *) diff --git a/theories/NArith/Nsqrt_def.v b/theories/NArith/Nsqrt_def.v index 1db7149419d5..0054f7e63374 100644 --- a/theories/NArith/Nsqrt_def.v +++ b/theories/NArith/Nsqrt_def.v @@ -10,6 +10,7 @@ Require Import BinNat. +Attributes deprecated(since="8.19", note="Require BinNat instead."). (** Obsolete file, see [BinNat] now, only compatibility notations remain here. *)