I haven't reproduced this, but I built Coq with
Set Nested Proofs Allowed. in
.coqrc, and it seems to have leaked into the Coq stdlib... I've seen it for instance in:
Test Nested Proofs Allowed. (* off *) From Ltac2 Require Import Ltac2. Test Nested Proofs Allowed. (* on *)
that might be due to
(flags -w -deprecated-native-compiler-option) instead of
(flags :standard -w -deprecated-native-compiler-option) — the former will omit
-q from the
coqc command line, so I think such a leak is expected?
what coq version?
Also Set with default locality shouldn't have an effect beyond the current module
Coq 8.16, and
#[global] Set Nested Proofs Allowed. — _that_ is on me
yeah I guess ltac2 didn't have -q
dune 3.6.1, but I understand that's only used by
I've learned this by forgetting
:standard a few times. Anyway, coq master replaces that by dunestrap, checking there
dunestrap gets this right. Nothing to do here...
FWIW, (untested) fix for 8.16, AFAICT: https://github.com/Blaisorblade/coq/commit/cff7918c92e5fc02472414b87e5baf725bae5ba9.
Paolo Giarrusso has marked this topic as resolved.
hmm, isn't the lesson here is that we should be vigilant for any missing
dune files? (Those
dune that specify
Please do upate the
dune.disabled files we do have there however.
Last updated: Dec 07 2023 at 06:38 UTC