Stream: Coq devs & plugin devs

Topic: Admitted used variables


view this post on Zulip Gaëtan Gilbert (Mar 27 2022 at 11:32):

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.

view this post on Zulip Enrico Tassi (Mar 27 2022 at 13:49):

proof using?
Anyway this is probably the case since the engine moved from metas to evars, since x is in scope.

view this post on Zulip Ana de Almeida Borges (Mar 28 2022 at 09:32):

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