Skip to content

Remove dec_agree and cofeT and use Coq #[deprecated] attribute for iAlways

Ralf Jung requested to merge ci/ralf/deprecated into master

Fixes #296 (closed)

I also just deleted things that have been in deprecated.v for years we cannot use #[deprecated] for all of them as old Coq did not support that attribute on Notation).

Edited by Ralf Jung

Merge request reports