From 4311fb24e79925229a466c4fdad6f6755a9ff75e Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Thu, 5 Mar 2026 20:10:31 +0100
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21611

---
 theories/xmathcomp/various.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/xmathcomp/various.v b/theories/xmathcomp/various.v
index 7dcf7cf..a942b93 100644
--- a/theories/xmathcomp/various.v
+++ b/theories/xmathcomp/various.v
@@ -734,7 +734,7 @@ HB.instance Definition _ :=
   GRing.isMultiplicative.Build L (subvs_of {:L}) (vsproj {:L})
     vsproj_is_multiplicative.
 
-Definition vssub (k K : {vspace L}) of (k <= K)%VS :
+Definition vssub (k K : {vspace L}) & (k <= K)%VS :
   subvs_of k -> subvs_of K := vsproj _ \o vsval.
 
 Variables (k K : {subfield L}) (kK : (k <= K)%VS).