ssreflect `[^ ident ]` pattern does not behave as documented when used after `elim`

[RalfJung]

Description of the problem

While debugging https://github.com/coq/coq/issues/16388, I encountered for the first time the [^ ident ] pattern. I was pointed at the documentation, but the behavior I see does not match what is documented, so I am unable to form a mental model of what this pattern is supposed to do. Consider:

From Coq Require Import String.
From Coq.ssr Require Export ssreflect.

Inductive val :=
  | PairV (v1 v2 : val).

Inductive expr :=
  | Call (e1 : expr) (e2 : expr)
  | If (e0 e1 e2 : expr)
  .

Section test.
  Context (subst : string -> val -> expr -> expr).

  Lemma to_expr_subst x v e :
    subst x v e = subst x v e.
  Proof.
    elim: e => /= [^ e].

What I would expect is that "It performs a case analysis on the top variable and introduces, in one go, all the variables coming from the case analysis". So, basically I should be able to write elim: e; simpl; intro [] instead and it should be basically the same as elim: e => /= [^ e] except that the things are named differently. However what actually happens is that it introduces a different number of variables in each of the newly created goals. It's 4 in the first goal and 6 in the second goal. And it doesn't perform any case distinction at all! It just magically introduces exactly as many things as the elim added.

The documentation says something about a special case when 'the intro pattern immediately follows a call to elim with a custom eliminator', but that is not the case here.

Coq Version

8.15.2

[Blaisorblade]

The relevant doc is https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html#block-introduction.

I agree this quote is not accurate:

It performs a case analysis on the top variable and introduces, in one go, all the variables coming from the case analysis.

but what does happen is that, if you have another tactic that performs a case analysis (EDIT: like elim), this introduces all the variables coming from the case analysis.

[Blaisorblade]

The documentation says something about a special case when 'the intro pattern immediately follows a call to elim with a custom eliminator', but that is not the case here.

That special case, AFAICT, is just about a different way to pick the names to introduce. Either way, case: t => [^ e] should introduce more or less as many variables as destruct t would introduce; I forget what happens with the induction hypotheses.

I took the liberty to tag this as a documentation bug, because the behavior and the text date back to https://github.com/coq/coq/pull/6705 — and I think the behavior is as intended, while the text is just sloppy.

[RalfJung]

I agree, the behavior is probably as intended, just not as documented.