Add quotation API for context and global_env_ext #2437

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

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

The default and global localities for this command outside sections

Could not enable unknown warning notation_overridden