MetaCoq CI

Merge branch 'coq-8.17-updates-8.16' into coq-8.18 #2419

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.