Adapt to rocq-prover/rocq#21987 (clear checks that ids are bound even when from match goal)

[SkySkimmer]

No description provided.

[xavierleroy]

Thanks for the early notice and for the patch.

Just curious: the "clear" was to ensure that the same hypothesis is destructed at most once. If "clear" fails, what prevents the "repeat" to loop forever?

[SkySkimmer]

Nothing I guess, but it doesn't seem to happen in practice (see green CI).

AFAICT for it to loop H would need to be a section variable (otherwise destruct would clear it) and would need to appear in the goal (to make clear fail).

[xavierleroy]

Gosh, you're right, destruct H already removes H, so clear H is useless. (Probably a leftover from an early version of this code that used elim instead of destruct.) I'll just remove clear H, then.

[xavierleroy]

Works great without clear H (commit 2d1d75f). Thanks again for the report!