Stream: Coq users

Topic: Global Qed

Ralf Jung (May 20 2021 at 17:01):

Is this code deliberately accepted, or is this a bug?

Lemma test: True.
Proof.
exact I.
Global Qed.

Michael Soegtrop (May 20 2021 at 19:45):

It is documented that Lemma & Co can take local and with that also global attributes. Since Qed is the command which actually saves the lemma in the environment, it is not that inconsequential, that it takes local and global attributes as well. The saving of the lemma in the environment can be changed at the point of Qed in other ways, say the name with Save. If one can change the name at this point, why not also the global/local?

Gaëtan Gilbert (May 20 2021 at 19:52):

it's bugged, it just ignores the attribute

Lemma foo : Prop.
Proof.
  exact True.
#[potato] Qed.

is also accepted...

Théo Zimmermann (May 20 2021 at 19:52):

But does Local Qed actually works and do anything? It sure isn't documented, so it is at least a documentation issue.

Enrico Tassi (May 20 2021 at 20:03):

I think we should give an error.

Emilio Jesús Gallego Arias (May 20 2021 at 20:52):

Théo Zimmermann said:

But does Local Qed actually works and do anything? It sure isn't documented, so it is at least a documentation issue.

As noted by Gaëtan it does nothing:

Emilio Jesús Gallego Arias (May 20 2021 at 20:53):

  | VernacEndProof pe ->
    VtCloseProof (vernac_end_proof pe)

Emilio Jesús Gallego Arias (May 20 2021 at 20:53):

let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function
  | Admitted ->
    Declare.Proof.save_admitted ~pm ~proof:lemma
  | Proved (opaque,idopt) ->
    let pm, _ = Declare.Proof.save ~pm ~proof:lemma ~opaque ~idopt
    in pm

and indeed there is little support for doing anything else.

Théo Zimmermann (May 21 2021 at 10:02):

Emilio Jesús Gallego Arias said:

Théo Zimmermann said:

But does Local Qed actually works and do anything? It sure isn't documented, so it is at least a documentation issue.

As noted by Gaëtan it does nothing:

Indeed, I was answering to Michael. Note that our messages were posted at the same time.

Ralf Jung (May 21 2021 at 17:35):

All right, opened a bug: https://github.com/coq/coq/issues/14360

Last updated: Apr 20 2024 at 12:02 UTC