From 78e50d7b623ac9dbe62d3d669f9904fec7e7f5f0 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Wed, 7 Jan 2026 14:24:21 +0100 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21478 --- secure_example/LabelledAsmCombinators.v | 6 +++--- theories/Basics/Basics.v | 14 +++++++------- tutorial/AsmCombinators.v | 6 +++--- 3 files changed, 13 insertions(+), 13 deletions(-) diff --git a/secure_example/LabelledAsmCombinators.v b/secure_example/LabelledAsmCombinators.v index d009e604..a876c0a4 100644 --- a/secure_example/LabelledAsmCombinators.v +++ b/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? *) diff --git a/theories/Basics/Basics.v b/theories/Basics/Basics.v index c25cbca0..c178f97a 100644 --- a/theories/Basics/Basics.v +++ b/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} diff --git a/tutorial/AsmCombinators.v b/tutorial/AsmCombinators.v index c4f827c6..d7ebaff0 100644 --- a/tutorial/AsmCombinators.v +++ b/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? *)