Stream: Coq users

Topic: Warning on `Variable` outside of `Section`, but not on `Cont


view this post on Zulip Yannick Forster (Jun 16 2022 at 10:21):

The documentation of Context says 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?

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 10:22):

we found that some people use Context to declare axioms

view this post on Zulip Yannick Forster (Jun 16 2022 at 10:24):

So maybe my bug report should then target the doc to make this transparent?

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 10:24):

sure

view this post on Zulip Gaëtan Gilbert (Jun 16 2022 at 10:24):

or you can directly make a PR


Last updated: Mar 28 2024 at 19:02 UTC