Int63 numbers are not captured by patterns in proofs

[mgbedmar]

Description of the problem

Trying to capture an Int63 number X in a proof using a pattern fails with Error: term X does not match any subterm in the goal.

Example:

Require Import Int63 ssreflect ssrfun ssrbool.

Lemma test : 43%int63 = (42 + 1)%int63.
Proof. set X := 43%int63. (* does not capture int63 *)

Coq Version

Coq 8.11.2

[ppedrot]

set uses the legacy unification engine, so it's probably been forgotten to add the relevant parts in there.

[gares]

This is about the set of SSR, which uses ssrmatching that has never been ported to the new term constructors.
I guess it is sufficient to fix this:

coq/plugins/ssrmatching/ssrmatching.ml

Lines 360 to 362 in e0b8b46

	let isRigid c = match kind c with
	| Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true
	| _ -> false

and return true also on native int/float/arrays