Ali Caglayan (Feb 08 2023 at 21:01): Ali Caglayan (Feb 08 2023 at 21:01):Why can't I #[bypass_check(guard)] inside a section? Is the ability to skip the guard condition not handled by cooking?
Ali Caglayan (Feb 08 2023 at 21:02):Specifically I get an error message like this:
Changing typing flags inside sections is not allowed.
because the typing flags are attached to definitions, so the typing flags used to check the variables would get lost
see https://github.com/coq/coq/issues/14317
Pierre-Marie Pédrot (Feb 10 2023 at 07:52):FTR attaching this flag to the definition is broken because it breaks SR (e.g. through module inline).
Pierre-Marie Pédrot (Feb 10 2023 at 07:52):I have a beginning of patch where this data is attached to the (co)fixpoints instead, which is semantically much better behaved.
Last updated: Oct 04 2023 at 21:01 UTC