Adapt to rocq-prover/rocq#20810.

[ppedrot]

This is backwards compatible.

[Copilot]

Pull Request Overview

This PR adapts the proof in PrimStringAxioms.v.in to reference the updated eqb from the PrimInt63 module, aligning with upstream changes in rocq-prover/rocq#20810 while preserving backwards compatibility.

• Qualify eqb in the proof to avoid ambiguity after the upstream refactor.

Comments suppressed due to low confidence (1)

theories/core/PrimStringAxioms.v.in:21

• [nitpick] Consider importing PrimInt63.eqb (e.g., Import PrimInt63.) or opening a local module at the top of the file to avoid fully qualifying eqb each time and improve readability.

#[skip="8.20"]   move: (eqb_correct x y); case: PrimInt63.eqb => [/(_ isT)->|_].

[gares]

Thanks @copilot your wisdom has no match!