Coq: `Proof <term>.` fails if it follows a non-Lemma-like command

[erikmd]

Description of the problem

If there is a (setting, query, ...) vernacular between Goal/Lemma and Proof <term>., then the proof term is rejected.

MWE using coqtop:

Lemma test : True.
Check 0. (* or  Set Printing All.  or … *)
Proof I.
(* Toplevel input, characters 0-8:
   > Proof I.
   > ^^^^^^^^
   Error:  (in proof test): Attempt to save an incomplete proof *)

This is reproducible with Coq 8.11, 8.10, 8.9... as long as the Proof I. command does not immediately follows Lemma …

Initially reported in the PG bug tracker by @mwuttke97 − https://github.com/ProofGeneral/PG/issues/498

Cc @Matafou @cpitclaudel @monnier FYI

Coq Version

$ coqtop -v
The Coq Proof Assistant, version 8.11.1 (April 2020)
compiled on Apr 9 2020 18:18:55 with OCaml 4.05.0

on Debian GNU/Linux

[Zimmi48]

I think this issue is more or less known and there is no intent to fix it. But rather to deprecate and remove the Proof <term> command as soon as Lemma := (cf. coq/ceps#42) is available.

[Zimmi48]

This is possibly a duplicate but Proof <term> is too hard to search for me to dig up the relevant issue.

[erikmd]

@Zimmi48 indeed, I found there are at least 2 duplicates :)

• https://github.com/coq/coq/issues/5592
• https://github.com/coq/coq/issues/8229

but as these two issues are a bit more specific (they only speak of Unset Silent), would it make sense to close them as duplicate, then close #12444 as wontfix (now or later)?

[Zimmi48]

Sure!

[erikmd]

done, I didn't close #12444 as wont-fix for the time being, but feel free to do so when you see fit

[Zimmi48]

I am indeed closing as "won't fix", but this time I am adding proper documentation of this known issue to its description in the refman (see #12450).