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

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

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?

it's bugged, it just ignores the attribute

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

is also accepted...

But does `Local Qed`

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

I think we should give an error.

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:

```
| VernacEndProof pe ->
VtCloseProof (vernac_end_proof pe)
```

```
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.

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.

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

Last updated: Jun 18 2024 at 22:01 UTC