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 *.