Yannick Forster (Jun 16 2022 at 10:21): 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?
Gaëtan Gilbert (Jun 16 2022 at 10:22):we found that some people use Context to declare axioms
Yannick Forster (Jun 16 2022 at 10:24):So maybe my bug report should then target the doc to make this transparent?
Gaëtan Gilbert (Jun 16 2022 at 10:24):sure
Gaëtan Gilbert (Jun 16 2022 at 10:24):or you can directly make a PR
Last updated: Oct 13 2024 at 01:02 UTC