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.
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: Dec 07 2023 at 18:01 UTC