Ssreflect have construct failing with Incorrect number of goals

[jouvelot]

The Ssreflect have construct fails in a somewhat unexpected way. The error message is

Error: Tactic failure: Incorrect number of goals (expected 1 tactic).

Note that adding a dummy argument to foo (i.e., have foo n:) makes it succeed.

From Coq Require Import ssreflect.

Lemma Peirce (A B : Prop) : ((A -> B) -> A) -> A.
Proof. 
have foo: A -> B.

Coq 8.13.0 (also fails in jsCoq)

[ejgallego]

I was able to reproduce this back to Coq 8.5 [thanks jsCoq :)] so indeed, not a new problem.

Note that this only happens when the goal in have is a subterm of the main goal. See even weirder behavior:

have foo n : A -> B.              (* works *)
have foo : A -> B := _ .          (* 100% bizarre *)