The documentation of
Declare variables in the context of the current section, like Variable, but also allowing implicit variables, Implicit generalization, and let-binders..
Variable triggers warnings if used outside of sections (https://coq.inria.fr/refman/language/core/assumptions.html#coq:warn.%E2%80%98ident%E2%80%99-is-declared-as-a-local-axiom), but
Context doesn't. Is there a reason or should I file a bug report?
we found that some people use Context to declare axioms
So maybe my bug report should then target the doc to make this transparent?
or you can directly make a PR
Last updated: Jan 31 2023 at 13:02 UTC