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.
Sorry about that.
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.
Sorry about that.