From 575315b0ddccec7b682b62d7e270da7e1c11c05d Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Wed, 7 Jan 2026 14:42:05 +0100
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21478

---
 theories/Systems/LiveLockServ.v  | 2 +-
 theories/Systems/LockServ.v      | 2 +-
 theories/Systems/PrimaryBackup.v | 6 +++---
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/Systems/LiveLockServ.v b/theories/Systems/LiveLockServ.v
index 899d782c..fd7674a0 100644
--- a/theories/Systems/LiveLockServ.v
+++ b/theories/Systems/LiveLockServ.v
@@ -106,7 +106,7 @@ Section LockServ.
                                  ServerNetHandler,
                                  ClientNetHandler,
                                  ClientIOHandler,
-                                 ServerIOHandler in *).
+                                 ServerIOHandler in * ).
 
 
 
diff --git a/theories/Systems/LockServ.v b/theories/Systems/LockServ.v
index ded59478..a0948fc0 100644
--- a/theories/Systems/LockServ.v
+++ b/theories/Systems/LockServ.v
@@ -91,7 +91,7 @@ Section LockServ.
                                  ServerNetHandler,
                                  ClientNetHandler,
                                  ClientIOHandler,
-                                 ServerIOHandler in *).
+                                 ServerIOHandler in * ).
 
 
 
diff --git a/theories/Systems/PrimaryBackup.v b/theories/Systems/PrimaryBackup.v
index 01783cbf..a757c2e0 100644
--- a/theories/Systems/PrimaryBackup.v
+++ b/theories/Systems/PrimaryBackup.v
@@ -824,11 +824,11 @@ Section PrimaryBackup.
 
   Definition network_invariant (net : @network _ PB_multi_params) : Prop :=
     (nwPackets net = [] /\ state (nwState net Primary) = state (nwState net Backup)) \/
-    (exists i is, nwPackets net = [mkPacket Primary Backup (BackItUp i)] /\
-               queue (nwState net Primary) = i :: is /\
+    (exists i si, nwPackets net = [mkPacket Primary Backup (BackItUp i)] /\
+               queue (nwState net Primary) = i :: si /\
                state (nwState net Primary) = state (nwState net Backup)) \/
     (nwPackets net = [mkPacket Backup Primary Ack] /\
-     exists i is, queue (nwState net Primary) = i :: is /\
+     exists i si, queue (nwState net Primary) = i :: si /\
                   snd (handler i (state (nwState net Primary))) = state (nwState net Backup)).
 
   Ltac prep := subst; simpl in *; try find_inversion; repeat find_rewrite; simpl in *.