Is this really what we want to happen?
Section S.
Variable x : nat.
Lemma bar : False.
Proof.
clear x.
Admitted.
Lemma foo : False.
Proof.
Admitted.
End S.
Check bar : False.
Check foo : nat -> False.
proof using?
Anyway this is probably the case since the engine moved from metas to evars, since x is in scope.
Umm, what is the point of using section variables if we need to manually decide whether they are useful with Proof using
? Is it just that it changes the default from "variable does not appear" to "variable appears"?
Last updated: Oct 13 2024 at 01:02 UTC