Adapt to rocq-prover/rocq#21478

Author: proux01

secure_example/LabelledAsmCombinators.v

@@ -86,10 +86,10 @@ Definition app_bks {A B C D : nat} (ab : bks A B) (cd : bks C D)
     end.
 
 (** Simple combinator to build a [block] from its instructions and branch operation. *)
-Fixpoint after {A: Type} (is : list instr) (bch : branch A) : block A :=
-  match is with
+Fixpoint after {A: Type} (si : list instr) (bch : branch A) : block A :=
+  match si with
   | nil => bbb bch
-  | i :: is => bbi i (after is bch)
+  | i :: si => bbi i (after si bch)
   end.
 
 (* SAZ: rationalize the names of the combinators? *)

theories/Basics/Basics.v

@@ -104,13 +104,13 @@ Polymorphic Class MonadIter (M : Type -> Type) : Type :=
 #[global] Instance MonadIter_stateT {M S} {MM : Monad M} {AM : MonadIter M}
   : MonadIter (stateT S M) :=
   fun _ _ step i => mkStateT (fun s =>
-    iter (fun is =>
-      let i := fst is in
-      let s := snd is in
-      is' <- runStateT (step i) s ;;
-      ret match fst is' with
-          | inl i' => inl (i', snd is')
-          | inr r => inr (r, snd is')
+    iter (fun si =>
+      let i := fst si in
+      let s := snd si in
+      si' <- runStateT (step i) s ;;
+      ret match fst si' with
+          | inl i' => inl (i', snd si')
+          | inr r => inr (r, snd si')
           end) (i, s)).
 
 #[global] Polymorphic Instance MonadIter_stateT0 {M S} {MM : Monad M} {AM : MonadIter M}

tutorial/AsmCombinators.v

@@ -79,10 +79,10 @@ Definition app_bks {A B C D : nat} (ab : bks A B) (cd : bks C D)
     end.
 
 (** Simple combinator to build a [block] from its instructions and branch operation. *)
-Fixpoint after {A: Type} (is : list instr) (bch : branch A) : block A :=
-  match is with
+Fixpoint after {A: Type} (si : list instr) (bch : branch A) : block A :=
+  match si with
   | nil => bbb bch
-  | i :: is => bbi i (after is bch)
+  | i :: si => bbi i (after si bch)
   end.
 
 (* SAZ: rationalize the names of the combinators? *)