[remix7531]

Floyd's printing notations for == and != sit at level 17, while ssreflect's eqtype and Stdlib's SetoidClass declare both at level 70. Rocq 9.1 rejects an only-printing notation at a different level once such a declaration is in scope, so on master both of these fail:

From mathcomp Require Import eqtype.
Require Import VST.floyd.proofauto.

From Stdlib Require Import SetoidClass.
Require Import VST.floyd.proofauto.

The first fails with: Notation "_ != _" is already defined at level 70 with arguments constr at next level, constr at next level while it is now required to be at level 17 with arguments constr at level 17, constr at level 16.

Importing Floyd first works, so developments that combine VST with MathComp or SSProve have to order their imports. libshrincs, formally verified SHRINCS implementations in VST and SSProve, documents this in proof/vst/base.v and proof/wots_plus_c.v.

I fixed this in Rocq: rocq-prover/rocq#22502 lets only-printing notations use different levels, with a warning (fixing rocq-prover/rocq#12465), and rocq-prover/rocq#22503 makes such notations take the parsing levels, so 0 == (1 + 1) keeps its parentheses. Both are merged into Rocq master, but VST builds with Rocq 9.1, so it needs this change as well.

This PR puts both notations at level 70 with no associativity, where Floyd's <, >, <= and >= already are. Goal display changes only around == and !=. Two expressions that master prints misleadingly now print correctly, and a plain comparison gains parentheses:

Clight term	master	this PR
Sset _v (Eunop Onotbool (Ebinop Oeq x y))	_v = !_x == _y;	_v = !(_x == _y);
Sset _v (Ebinop Oadd (Ebinop Oeq x y) 1)	_v = (_x == _y + (1));	_v = ((_x == _y) + (1));
Sset _v (Ebinop Oeq x y)	_v = _x == _y;	_v = (_x == _y);

Here x and y are Etempvar _x tint and Etempvar _y tint.

Tested on Rocq 9.1.1 at both bit sizes: make vst, make test and make assumptions.txt pass with unchanged assumptions, and both files above compile.