proof-goto-point does not work as a sequence of proof-assert-next-command-interactive

[anton-trunov]

When I go over the following snippet step-by-step (proof-assert-next-command-interactive) it works, i.e. foo gets defined.

Set Implicit Arguments.
Lemma foo (P : Prop) : P -> P.
Proof (fun p : P => p).
(* line 4 *)

But, if instead I put the point over line 4 and use proof-goto-point, I get

Error: Attempt to save an incomplete proof (in proof foo)

[cpitclaudel]

Which version of Coq and PG are you using? (both of these works for me on Coq 8.8.0 and PG e1b3efb8e8ace78af9a0459318a927a28574c92e, which isn't the latest master)

[anton-trunov]

Oh, sorry, I forgot to add Set Implicit Arguments. to the snippet. Without this addition I cannot reproduce it too.

I'm on Coq 8.8.1, PG b238dab7a2f8a52281a920df027c3dea4fc4b28c

[cpitclaudel]

Hmm, still works fine for me :/ Can you show the contents of the *Coq* buffer in the failing case?

[anton-trunov]

Here it is.

Welcome to Coq 8.8.1 (July 2018)

<prompt>Coq < 1 || 0 < </prompt>Add Search Blacklist "Private_" "_subproof". 

<prompt>Coq < 2 || 0 < </prompt>Set Printing Depth 50 . 

<prompt>Coq < 3 || 0 < </prompt>Remove Search Blacklist "Private_" "_subproof".  Add Search Blacklist "Private_" "_subproof". 

<prompt>Coq < 4 || 0 < </prompt>
<prompt>Coq < 5 || 0 < </prompt>Set Printing Width 84.

<prompt>Coq < 6 || 0 < </prompt>Set Silent. 

<prompt>Coq < 7 || 0 < </prompt>Set Implicit Arguments.

<prompt>Coq < 8 || 0 < </prompt>Lemma foo (P : Prop) : P -> P.

<prompt>foo < 9 |foo| 0 < </prompt>Unset Silent. 

<prompt>foo < 11 |foo| 0 < </prompt>Proof (fun p : P => p).
Toplevel input, characters 15-38:
> Proof (fun p : P => p).
> ^^^^^^^^^^^^^^^^^^^^^^^
Error: Attempt to save an incomplete proof (in proof foo)

<prompt>foo < 11 |foo| 0 < </prompt>

[cpitclaudel]

Can you try reproducing this on the terminal, by typing these same commands in coqtop?

[anton-trunov]

Yes, you are right, it's on the coqtop side, apparently. I filed issue #8229 in Coq's GitHub.