[SOLVED] How can one handle by case analysis a boolP expression in Coq/ssreflect?

How can one handle by case analysis a boolP expression in Coq/ssreflect?

I'm puzzled by this simple lemma (a simplified version of what I'm trying to do).

From mathcomp Require Import all_ssreflect.

Lemma foo (bar : bool) : match boolP bar with
  | @AltTrue _ _ baz => (fun=> 1) baz
  | @AltFalse _ _ _ => 1
  end = 1.
Proof.
case x: (boolP bar).

How should I address the case analysis on the match expression? Where does this b come from in the error message below?

Error: Illegal application: 
The term "@eq" of type "∀ A : Type, A → A → Prop"
cannot be applied to the terms
 "alt_spec bar bar bar" : "Set"
 "boolP bar" : "alt_spec bar bar bar"
 "a" : "alt_spec bar bar b"
The 3rd term has type "alt_spec bar bar b" which should be coercible to 
"alt_spec bar bar bar".

I'm using an old 8.17 version of Rocq, with mathcomp 1.17. This also occurs on the last version of Rocq (as per jsCoq).

Solution

A non-ssreflect way of proceeding here is to simply destruct (boolP bar). I would presume that the ssreflect-case tactic is buggy here but do not know enough about ssreflect to be certain.