MetaCoq CI

move implement_box_transformation to coq-malfunction #2450

Annotations

10 warnings

Tactic Notation revert dependent (hyp) is deprecated since 8.18.

Huctx' is declared opaque (Qed) but this is not fully respected

HC' is declared opaque (Qed) but this is not fully respected inside

HG' is declared opaque (Qed) but this is not fully respected inside

The default and global localities for this command outside sections

Could not enable unknown warning notation_overridden

Notation "_ { _ := _ }" was already used.

Notation "_ ,,, _" was already used.