Use Coq deprecation attribute to implement deprecations
Now that Iris only supports Coq 8.9+, we can use the #[deprecated]
attribute on any deprecated tactics or definitions. Deprecation warnings are nice because they can be either suppressed with -w -deprecated
or turned into an error with -w +deprecated
.
This immediately applies to:
iAlways
-
algebra/deprecated.v
'scofeT
anddec_agree
(dec_agree
may need to be wrapped in a notation first)
Iris also has a few dynamic deprecations that Coq currently doesn't support. The IPM can detect these but currently (due to Coq limitations) has no way to raise a user-level deprecation warning.
- The deprecated
!#
intro pattern is parsed asTIntuitionisticIntro
but then treated the same asTModalIntro
. - The
*
specialization pattern is deprecated and triggers a deprecation message usingidtac
.