MetaCoq CI

Add quotation API for context and global_env_ext (#996) #2438

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.