diff --git a/raft-proofs/AllEntriesCandidateEntriesProof.v b/raft-proofs/AllEntriesCandidateEntriesProof.v
index b2f0b39..e5ba760 100644
--- a/raft-proofs/AllEntriesCandidateEntriesProof.v
+++ b/raft-proofs/AllEntriesCandidateEntriesProof.v
@@ -4,7 +4,7 @@ From VerdiRaft Require Import CroniesCorrectInterface CroniesTermInterface.
 From VerdiRaft Require Import AllEntriesTermSanityInterface SpecLemmas.
 From VerdiRaft Require Import RefinementSpecLemmas AllEntriesCandidateEntriesInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AllEntriesCandidateEntries.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/AllEntriesIndicesGt0Proof.v b/raft-proofs/AllEntriesIndicesGt0Proof.v
index 86b0eef..bd55956 100644
--- a/raft-proofs/AllEntriesIndicesGt0Proof.v
+++ b/raft-proofs/AllEntriesIndicesGt0Proof.v
@@ -4,7 +4,7 @@ From VerdiRaft Require Import CommonDefinitions RefinementSpecLemmas.
 From VerdiRaft Require Import TermsAndIndicesFromOneLogInterface.
 From VerdiRaft Require Import AllEntriesIndicesGt0Interface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AllEntriesIndicesGt0.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/AllEntriesLeaderLogsProof.v b/raft-proofs/AllEntriesLeaderLogsProof.v
index db8bf9a..2ad413b 100644
--- a/raft-proofs/AllEntriesLeaderLogsProof.v
+++ b/raft-proofs/AllEntriesLeaderLogsProof.v
@@ -7,7 +7,7 @@ From VerdiRaft Require Import AllEntriesLogInterface LeaderSublogInterface.
 From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface.
 From VerdiRaft Require Import AllEntriesLeaderLogsInterface.
 
-Local Arguments update {_} {_} {_} _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} {_} _ _ _ _ : simpl never.
 
 Section AllEntriesLeaderLogs.
 
diff --git a/raft-proofs/AllEntriesLeaderLogsTermProof.v b/raft-proofs/AllEntriesLeaderLogsTermProof.v
index e606288..30dbf8b 100644
--- a/raft-proofs/AllEntriesLeaderLogsTermProof.v
+++ b/raft-proofs/AllEntriesLeaderLogsTermProof.v
@@ -3,7 +3,7 @@ From VerdiRaft Require Import RefinementSpecLemmas SpecLemmas.
 From VerdiRaft Require Import AllEntriesLeaderLogsTermInterface.
 From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AllEntriesLeaderLogsTerm.
 
diff --git a/raft-proofs/AllEntriesLeaderSublogProof.v b/raft-proofs/AllEntriesLeaderSublogProof.v
index 77d9d03..3f04c30 100644
--- a/raft-proofs/AllEntriesLeaderSublogProof.v
+++ b/raft-proofs/AllEntriesLeaderSublogProof.v
@@ -8,7 +8,7 @@ From VerdiRaft Require Import AllEntriesCandidateEntriesInterface.
 From VerdiRaft Require Import VotesCorrectInterface CroniesCorrectInterface.
 From VerdiRaft Require Import LeaderSublogInterface OneLeaderPerTermInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AllEntriesLeaderSublog.
 
diff --git a/raft-proofs/AllEntriesLogMatchingProof.v b/raft-proofs/AllEntriesLogMatchingProof.v
index a18ee5b..d34e4ef 100644
--- a/raft-proofs/AllEntriesLogMatchingProof.v
+++ b/raft-proofs/AllEntriesLogMatchingProof.v
@@ -5,7 +5,7 @@ From VerdiRaft Require Import AllEntriesLeaderSublogInterface.
 From VerdiRaft Require Import LeaderSublogInterface RefinedLogMatchingLemmasInterface.
 From VerdiRaft Require Import AllEntriesLogMatchingInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AllEntriesLogMatching.
 
diff --git a/raft-proofs/AllEntriesLogProof.v b/raft-proofs/AllEntriesLogProof.v
index 4f6d234..062e560 100644
--- a/raft-proofs/AllEntriesLogProof.v
+++ b/raft-proofs/AllEntriesLogProof.v
@@ -10,7 +10,7 @@ From VerdiRaft Require Import OneLeaderLogPerTermInterface.
 From VerdiRaft Require Import LeaderLogsSortedInterface TermSanityInterface.
 From VerdiRaft Require Import AllEntriesTermSanityInterface AllEntriesLogInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AllEntriesLog.
 
diff --git a/raft-proofs/AllEntriesTermSanityProof.v b/raft-proofs/AllEntriesTermSanityProof.v
index 3a1cae5..b435fa2 100644
--- a/raft-proofs/AllEntriesTermSanityProof.v
+++ b/raft-proofs/AllEntriesTermSanityProof.v
@@ -1,7 +1,7 @@
 From VerdiRaft Require Import Raft RaftRefinementInterface SpecLemmas.
 From VerdiRaft Require Import RefinementSpecLemmas AllEntriesTermSanityInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AllEntriesTermSanity.
 
diff --git a/raft-proofs/AllEntriesVotesWithLogProof.v b/raft-proofs/AllEntriesVotesWithLogProof.v
index e32fb88..2c441bd 100644
--- a/raft-proofs/AllEntriesVotesWithLogProof.v
+++ b/raft-proofs/AllEntriesVotesWithLogProof.v
@@ -5,7 +5,7 @@ From VerdiRaft Require Import AllEntriesVotesWithLogInterface AllEntriesLogInter
 From VerdiRaft Require Import VotesWithLogTermSanityInterface VotesCorrectInterface.
 From VerdiRaft Require Import VotesVotesWithLogCorrespondInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AllEntriesVotesWithLog.
 
diff --git a/raft-proofs/AppendEntriesLeaderProof.v b/raft-proofs/AppendEntriesLeaderProof.v
index 0475f4f..399f8bb 100644
--- a/raft-proofs/AppendEntriesLeaderProof.v
+++ b/raft-proofs/AppendEntriesLeaderProof.v
@@ -4,7 +4,7 @@ From VerdiRaft Require Import AppendEntriesRequestsCameFromLeadersInterface.
 From VerdiRaft Require Import OneLeaderLogPerTermInterface LeaderLogsTermSanityInterface.
 From VerdiRaft Require Import OneLeaderPerTermInterface AppendEntriesLeaderInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AppendEntriesLeader.
 
diff --git a/raft-proofs/AppendEntriesReplySublogProof.v b/raft-proofs/AppendEntriesReplySublogProof.v
index 6731bec..f7e27ae 100644
--- a/raft-proofs/AppendEntriesReplySublogProof.v
+++ b/raft-proofs/AppendEntriesReplySublogProof.v
@@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft AppendEntriesReplySublogInterface.
 From VerdiRaft Require Import AppendEntriesRequestReplyCorrespondenceInterface.
 From VerdiRaft Require Import RaftRefinementInterface AppendEntriesLeaderInterface.
 
-Local Arguments update {_} {_} {_} _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} {_} _ _ _ _ : simpl never.
 
 Section AppendEntriesReplySublog.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/AppendEntriesRequestLeaderLogsProof.v b/raft-proofs/AppendEntriesRequestLeaderLogsProof.v
index 552782a..2c2e97a 100644
--- a/raft-proofs/AppendEntriesRequestLeaderLogsProof.v
+++ b/raft-proofs/AppendEntriesRequestLeaderLogsProof.v
@@ -5,7 +5,7 @@ From VerdiRaft Require Import SortedInterface LogMatchingInterface.
 From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface.
 From VerdiRaft Require Import NextIndexSafetyInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AppendEntriesRequestLeaderLogs.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v b/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v
index fe8b119..227e69e 100644
--- a/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v
+++ b/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v
@@ -3,7 +3,7 @@ From VerdiRaft Require Import Raft SpecLemmas.
 From VerdiRaft Require Import AppendEntriesRequestReplyCorrespondenceInterface.
 From Verdi Require Import DupDropReordering.
 
-Local Arguments update {_} {_} {_} _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} {_} _ _ _ _ : simpl never.
 
 Section AppendEntriesRequestReplyCorrespondence.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v b/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v
index b06467c..a290699 100644
--- a/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v
+++ b/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v
@@ -3,7 +3,7 @@ From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import LeadersHaveLeaderLogsInterface.
 From VerdiRaft Require Import AppendEntriesRequestsCameFromLeadersInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AppendEntriesRequestsCameFromLeaders.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/AppliedEntriesMonotonicProof.v b/raft-proofs/AppliedEntriesMonotonicProof.v
index 81b1eee..8439863 100644
--- a/raft-proofs/AppliedEntriesMonotonicProof.v
+++ b/raft-proofs/AppliedEntriesMonotonicProof.v
@@ -8,7 +8,7 @@ From VerdiRaft Require Import LeaderCompletenessInterface.
 From VerdiRaft Require Import LastAppliedCommitIndexMatchingInterface.
 From VerdiRaft Require Import SpecLemmas AppliedEntriesMonotonicInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AppliedEntriesMonotonicProof.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/AppliedImpliesInputProof.v b/raft-proofs/AppliedImpliesInputProof.v
index 61bcc80..9e5623c 100644
--- a/raft-proofs/AppliedImpliesInputProof.v
+++ b/raft-proofs/AppliedImpliesInputProof.v
@@ -3,7 +3,7 @@ From VerdiRaft Require Import Raft CommonTheorems.
 From VerdiRaft Require Import TraceUtil OutputImpliesAppliedInterface.
 From VerdiRaft Require Import SpecLemmas AppliedImpliesInputInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section AppliedImpliesInputProof.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/CandidateEntriesProof.v b/raft-proofs/CandidateEntriesProof.v
index 2a42ae7..90f8f57 100644
--- a/raft-proofs/CandidateEntriesProof.v
+++ b/raft-proofs/CandidateEntriesProof.v
@@ -4,7 +4,7 @@ From VerdiRaft Require Import VotesCorrectInterface TermSanityInterface.
 From VerdiRaft Require Import CroniesTermInterface RefinementCommonTheorems.
 From VerdiRaft Require Import SpecLemmas CandidateEntriesInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section CandidateEntriesProof.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/CandidateTermGtLogProof.v b/raft-proofs/CandidateTermGtLogProof.v
index a96730b..c9070d1 100644
--- a/raft-proofs/CandidateTermGtLogProof.v
+++ b/raft-proofs/CandidateTermGtLogProof.v
@@ -1,7 +1,7 @@
 From VerdiRaft Require Import Raft SpecLemmas TermSanityInterface.
 From VerdiRaft Require Import CandidateTermGtLogInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section CandidateTermGtLog.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/CausalOrderPreservedProof.v b/raft-proofs/CausalOrderPreservedProof.v
index 1e82961..e60b66d 100644
--- a/raft-proofs/CausalOrderPreservedProof.v
+++ b/raft-proofs/CausalOrderPreservedProof.v
@@ -5,7 +5,7 @@ From VerdiRaft Require Import OutputImpliesAppliedInterface.
 From VerdiRaft Require Import AppliedImpliesInputInterface.
 From VerdiRaft Require Import AppliedEntriesMonotonicInterface.
 
-Local Arguments update {_} {_} {_} _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} {_} _ _ _ _ : simpl never.
 
 Section CausalOrderPreserved.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/CroniesTermProof.v b/raft-proofs/CroniesTermProof.v
index 3f4beee..d1c98f9 100644
--- a/raft-proofs/CroniesTermProof.v
+++ b/raft-proofs/CroniesTermProof.v
@@ -1,7 +1,7 @@
 From VerdiRaft Require Import Raft RaftRefinementInterface.
 From VerdiRaft Require Import CommonTheorems CroniesTermInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section CroniesTermProof.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/CurrentTermGtZeroProof.v b/raft-proofs/CurrentTermGtZeroProof.v
index 3761037..31c6109 100644
--- a/raft-proofs/CurrentTermGtZeroProof.v
+++ b/raft-proofs/CurrentTermGtZeroProof.v
@@ -1,6 +1,6 @@
 From VerdiRaft Require Import Raft SpecLemmas CurrentTermGtZeroInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section CurrentTermGtZero.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/EveryEntryWasCreatedProof.v b/raft-proofs/EveryEntryWasCreatedProof.v
index d3524ae..f22080a 100644
--- a/raft-proofs/EveryEntryWasCreatedProof.v
+++ b/raft-proofs/EveryEntryWasCreatedProof.v
@@ -5,7 +5,7 @@ From VerdiRaft Require Import EveryEntryWasCreatedInterface.
 From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import CommonTheorems.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section EveryEntryWasCreated.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/GhostLogAllEntriesProof.v b/raft-proofs/GhostLogAllEntriesProof.v
index a5c5524..57ad97e 100644
--- a/raft-proofs/GhostLogAllEntriesProof.v
+++ b/raft-proofs/GhostLogAllEntriesProof.v
@@ -5,7 +5,7 @@ From VerdiRaft Require Import RaftMsgRefinementInterface.
 From VerdiRaft Require Import InLogInAllEntriesInterface.
 From VerdiRaft Require Import GhostLogAllEntriesInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section GhostLogAllEntriesProof.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/GhostLogCorrectProof.v b/raft-proofs/GhostLogCorrectProof.v
index a786da1..a0d8339 100644
--- a/raft-proofs/GhostLogCorrectProof.v
+++ b/raft-proofs/GhostLogCorrectProof.v
@@ -5,7 +5,7 @@ From VerdiRaft Require Import NextIndexSafetyInterface.
 From VerdiRaft Require Import RefinedLogMatchingLemmasInterface.
 From VerdiRaft Require Import GhostLogCorrectInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section GhostLogCorrectProof.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/GhostLogLogMatchingProof.v b/raft-proofs/GhostLogLogMatchingProof.v
index 32f8f26..e55a9b3 100644
--- a/raft-proofs/GhostLogLogMatchingProof.v
+++ b/raft-proofs/GhostLogLogMatchingProof.v
@@ -10,7 +10,7 @@ From VerdiRaft Require Import AllEntriesLeaderSublogInterface.
 From VerdiRaft Require Import GhostLogAllEntriesInterface.
 From VerdiRaft Require Import GhostLogLogMatchingInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section GhostLogLogMatching.
 
diff --git a/raft-proofs/GhostLogsLogPropertiesProof.v b/raft-proofs/GhostLogsLogPropertiesProof.v
index 12c2502..cd37b35 100644
--- a/raft-proofs/GhostLogsLogPropertiesProof.v
+++ b/raft-proofs/GhostLogsLogPropertiesProof.v
@@ -2,7 +2,7 @@ From Verdi Require Import GhostSimulations.
 From VerdiRaft Require Import Raft RaftMsgRefinementInterface.
 From VerdiRaft Require Import GhostLogsLogPropertiesInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section GhostLogsLogProperties.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/InLogInAllEntriesProof.v b/raft-proofs/InLogInAllEntriesProof.v
index 91f731e..ab78971 100644
--- a/raft-proofs/InLogInAllEntriesProof.v
+++ b/raft-proofs/InLogInAllEntriesProof.v
@@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface.
 From VerdiRaft Require Import CommonTheorems SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import InLogInAllEntriesInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section InLogInAllEntries.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/InputBeforeOutputProof.v b/raft-proofs/InputBeforeOutputProof.v
index fe0df41..60495c0 100644
--- a/raft-proofs/InputBeforeOutputProof.v
+++ b/raft-proofs/InputBeforeOutputProof.v
@@ -8,7 +8,7 @@ From VerdiRaft Require Import SortedInterface LogMatchingInterface.
 From VerdiRaft Require Import StateMachineSafetyInterface MaxIndexSanityInterface.
 From VerdiRaft Require Import UniqueIndicesInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section InputBeforeOutput.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/LastAppliedLeCommitIndexProof.v b/raft-proofs/LastAppliedLeCommitIndexProof.v
index b4a391f..80b0acc 100644
--- a/raft-proofs/LastAppliedLeCommitIndexProof.v
+++ b/raft-proofs/LastAppliedLeCommitIndexProof.v
@@ -1,7 +1,7 @@
 From VerdiRaft Require Import Raft LastAppliedLeCommitIndexInterface.
 From VerdiRaft Require Import SpecLemmas CommonTheorems.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LastAppliedLeCommitIndex.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/LeaderLogsCandidateEntriesProof.v b/raft-proofs/LeaderLogsCandidateEntriesProof.v
index 922c904..dc4589d 100644
--- a/raft-proofs/LeaderLogsCandidateEntriesProof.v
+++ b/raft-proofs/LeaderLogsCandidateEntriesProof.v
@@ -7,7 +7,7 @@ From VerdiRaft Require Import LeaderLogsTermSanityInterface.
 From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import LeaderLogsCandidateEntriesInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section CandidateEntriesInterface.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/LeaderLogsContiguousProof.v b/raft-proofs/LeaderLogsContiguousProof.v
index aa24476..9a5e0d5 100644
--- a/raft-proofs/LeaderLogsContiguousProof.v
+++ b/raft-proofs/LeaderLogsContiguousProof.v
@@ -3,7 +3,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface CommonTheorems.
 From VerdiRaft Require Import LeaderLogsContiguousInterface.
 From VerdiRaft Require Import LogMatchingInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LeaderLogsContiguous.
 
diff --git a/raft-proofs/LeaderLogsLogMatchingProof.v b/raft-proofs/LeaderLogsLogMatchingProof.v
index 6b4b035..a116095 100644
--- a/raft-proofs/LeaderLogsLogMatchingProof.v
+++ b/raft-proofs/LeaderLogsLogMatchingProof.v
@@ -10,7 +10,7 @@ From VerdiRaft Require Import LeaderLogsContiguousInterface.
 From VerdiRaft Require Import TermsAndIndicesFromOneInterface.
 From VerdiRaft Require Import LeaderLogsLogMatchingInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LeaderLogsLogMatching.
 
diff --git a/raft-proofs/LeaderLogsLogPropertiesProof.v b/raft-proofs/LeaderLogsLogPropertiesProof.v
index e0850d5..d5bb9cb 100644
--- a/raft-proofs/LeaderLogsLogPropertiesProof.v
+++ b/raft-proofs/LeaderLogsLogPropertiesProof.v
@@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface SpecLemmas.
 From VerdiRaft Require Import LeaderLogsLogPropertiesInterface.
 From VerdiRaft Require Import RefinementSpecLemmas.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LeaderLogsLogProperties.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/LeaderLogsPreservedProof.v b/raft-proofs/LeaderLogsPreservedProof.v
index 709274e..73925e8 100644
--- a/raft-proofs/LeaderLogsPreservedProof.v
+++ b/raft-proofs/LeaderLogsPreservedProof.v
@@ -8,7 +8,7 @@ From VerdiRaft Require Import OneLeaderLogPerTermInterface.
 From VerdiRaft Require Import VotesCorrectInterface.
 From VerdiRaft Require Import CroniesCorrectInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LeaderLogsPreserved.
 
diff --git a/raft-proofs/LeaderLogsSortedProof.v b/raft-proofs/LeaderLogsSortedProof.v
index ecd861f..eacee28 100644
--- a/raft-proofs/LeaderLogsSortedProof.v
+++ b/raft-proofs/LeaderLogsSortedProof.v
@@ -4,7 +4,7 @@ From VerdiRaft Require Import CommonDefinitions SpecLemmas.
 From VerdiRaft Require Import LeaderLogsSortedInterface.
 From VerdiRaft Require Import SortedInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LeaderLogsSorted.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/LeaderLogsSublogProof.v b/raft-proofs/LeaderLogsSublogProof.v
index 662721f..282527a 100644
--- a/raft-proofs/LeaderLogsSublogProof.v
+++ b/raft-proofs/LeaderLogsSublogProof.v
@@ -10,7 +10,7 @@ From VerdiRaft Require Import VotesCorrectInterface.
 From VerdiRaft Require Import RefinementCommonTheorems.
 From VerdiRaft Require Import LeaderLogsSublogInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LeaderLogsSublog.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/LeaderLogsTermSanityProof.v b/raft-proofs/LeaderLogsTermSanityProof.v
index 699fefd..fac9ccd 100644
--- a/raft-proofs/LeaderLogsTermSanityProof.v
+++ b/raft-proofs/LeaderLogsTermSanityProof.v
@@ -4,7 +4,7 @@ From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import CandidateTermGtLogInterface.
 From VerdiRaft Require Import LeaderLogsTermSanityInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LeaderLogsTermSanity.
 
diff --git a/raft-proofs/LeaderLogsVotesWithLogProof.v b/raft-proofs/LeaderLogsVotesWithLogProof.v
index 7974e74..84c2adb 100644
--- a/raft-proofs/LeaderLogsVotesWithLogProof.v
+++ b/raft-proofs/LeaderLogsVotesWithLogProof.v
@@ -4,7 +4,7 @@ From VerdiRaft Require Import VotesReceivedMoreUpToDateInterface.
 From VerdiRaft Require Import RequestVoteReplyMoreUpToDateInterface.
 From VerdiRaft Require Import LeaderLogsVotesWithLogInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LeaderLogsVotesWithLog.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/LeadersHaveLeaderLogsProof.v b/raft-proofs/LeadersHaveLeaderLogsProof.v
index b550307..adf83a6 100644
--- a/raft-proofs/LeadersHaveLeaderLogsProof.v
+++ b/raft-proofs/LeadersHaveLeaderLogsProof.v
@@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface.
 From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import LeadersHaveLeaderLogsInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LeadersHaveLeaderLogs.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/LeadersHaveLeaderLogsStrongProof.v b/raft-proofs/LeadersHaveLeaderLogsStrongProof.v
index 0cd675a..68df943 100644
--- a/raft-proofs/LeadersHaveLeaderLogsStrongProof.v
+++ b/raft-proofs/LeadersHaveLeaderLogsStrongProof.v
@@ -1,7 +1,7 @@
 From VerdiRaft Require Import Raft RaftRefinementInterface CommonTheorems.
 From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LeadersHaveLeaderLogsStrong.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/LogAllEntriesProof.v b/raft-proofs/LogAllEntriesProof.v
index 7a4f306..0071ca4 100644
--- a/raft-proofs/LogAllEntriesProof.v
+++ b/raft-proofs/LogAllEntriesProof.v
@@ -4,7 +4,7 @@ From VerdiRaft Require Import RefinementSpecLemmas.
 From VerdiRaft Require Import TermSanityInterface.
 From VerdiRaft Require Import LogAllEntriesInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LogAllEntries.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/LogsLeaderLogsProof.v b/raft-proofs/LogsLeaderLogsProof.v
index 12a15c3..30deb6c 100644
--- a/raft-proofs/LogsLeaderLogsProof.v
+++ b/raft-proofs/LogsLeaderLogsProof.v
@@ -10,7 +10,7 @@ From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface.
 From VerdiRaft Require Import NextIndexSafetyInterface.
 From VerdiRaft Require Import SortedInterface LeaderLogsLogPropertiesInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section LogsLeaderLogs.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/MatchIndexAllEntriesProof.v b/raft-proofs/MatchIndexAllEntriesProof.v
index 0db4fbb..0b15d32 100644
--- a/raft-proofs/MatchIndexAllEntriesProof.v
+++ b/raft-proofs/MatchIndexAllEntriesProof.v
@@ -18,7 +18,7 @@ From VerdiRaft Require Import VotesCorrectInterface.
 From VerdiRaft Require Import CroniesCorrectInterface.
 From VerdiRaft Require Import MatchIndexAllEntriesInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section MatchIndexAllEntries.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/MatchIndexLeaderProof.v b/raft-proofs/MatchIndexLeaderProof.v
index ea2b656..459f052 100644
--- a/raft-proofs/MatchIndexLeaderProof.v
+++ b/raft-proofs/MatchIndexLeaderProof.v
@@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft SpecLemmas.
 From VerdiRaft Require Import NoAppendEntriesRepliesToSelfInterface.
 From VerdiRaft Require Import MatchIndexLeaderInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section MatchIndexLeader.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/MatchIndexSanityProof.v b/raft-proofs/MatchIndexSanityProof.v
index 165b9c1..be89013 100644
--- a/raft-proofs/MatchIndexSanityProof.v
+++ b/raft-proofs/MatchIndexSanityProof.v
@@ -3,7 +3,7 @@ From VerdiRaft Require Import AppendEntriesReplySublogInterface.
 From VerdiRaft Require Import MatchIndexSanityInterface.
 From VerdiRaft Require Import SortedInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section MatchIndexSanity.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/NextIndexSafetyProof.v b/raft-proofs/NextIndexSafetyProof.v
index e5d0a0d..b44a4a4 100644
--- a/raft-proofs/NextIndexSafetyProof.v
+++ b/raft-proofs/NextIndexSafetyProof.v
@@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft CommonTheorems SpecLemmas.
 From VerdiRaft Require Import AppendEntriesReplySublogInterface.
 From VerdiRaft Require Import SortedInterface NextIndexSafetyInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section NextIndexSafety.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/OneLeaderLogPerTermProof.v b/raft-proofs/OneLeaderLogPerTermProof.v
index 28c50c3..cac7b9f 100644
--- a/raft-proofs/OneLeaderLogPerTermProof.v
+++ b/raft-proofs/OneLeaderLogPerTermProof.v
@@ -10,7 +10,7 @@ From VerdiRaft Require Import VotesVotesWithLogCorrespondInterface.
 From VerdiRaft Require Import LeaderLogsTermSanityInterface.
 From VerdiRaft Require Import OneLeaderLogPerTermInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section OneLeaderLogPerTerm.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/OutputCorrectProof.v b/raft-proofs/OutputCorrectProof.v
index edf6501..f75f812 100644
--- a/raft-proofs/OutputCorrectProof.v
+++ b/raft-proofs/OutputCorrectProof.v
@@ -6,7 +6,7 @@ From VerdiRaft Require Import TraceUtil StateMachineCorrectInterface.
 From VerdiRaft Require Import SortedInterface LastAppliedCommitIndexMatchingInterface.
 From VerdiRaft Require Import LogMatchingInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section OutputCorrect.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/OutputGreatestIdProof.v b/raft-proofs/OutputGreatestIdProof.v
index 43d0557..07f20a2 100644
--- a/raft-proofs/OutputGreatestIdProof.v
+++ b/raft-proofs/OutputGreatestIdProof.v
@@ -8,7 +8,7 @@ From VerdiRaft Require Import LastAppliedCommitIndexMatchingInterface.
 From VerdiRaft Require Import TraceUtil SortedInterface.
 From VerdiRaft Require Import OutputGreatestIdInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section OutputGreatestId.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/OutputImpliesAppliedProof.v b/raft-proofs/OutputImpliesAppliedProof.v
index ea72539..e5892d2 100644
--- a/raft-proofs/OutputImpliesAppliedProof.v
+++ b/raft-proofs/OutputImpliesAppliedProof.v
@@ -6,7 +6,7 @@ From VerdiRaft Require Import MaxIndexSanityInterface.
 From VerdiRaft Require Import TraceUtil SortedInterface.
 From VerdiRaft Require Import OutputImpliesAppliedInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section OutputImpliesApplied.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/PrefixWithinTermProof.v b/raft-proofs/PrefixWithinTermProof.v
index 72b2600..8104615 100644
--- a/raft-proofs/PrefixWithinTermProof.v
+++ b/raft-proofs/PrefixWithinTermProof.v
@@ -14,7 +14,7 @@ From VerdiRaft Require Import AllEntriesLogMatchingInterface.
 From VerdiRaft Require Import AppendEntriesRequestTermSanityInterface.
 From VerdiRaft Require Import AllEntriesLeaderSublogInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section PrefixWithinTerm.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/PrevLogCandidateEntriesTermProof.v b/raft-proofs/PrevLogCandidateEntriesTermProof.v
index 08491d3..3957fda 100644
--- a/raft-proofs/PrevLogCandidateEntriesTermProof.v
+++ b/raft-proofs/PrevLogCandidateEntriesTermProof.v
@@ -7,7 +7,7 @@ From VerdiRaft Require Import RefinementSpecLemmas.
 From VerdiRaft Require Import RefinementCommonTheorems.
 From VerdiRaft Require Import PrevLogCandidateEntriesTermInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section PrevLogCandidateEntriesTerm.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/RequestVoteMaxIndexMaxTermProof.v b/raft-proofs/RequestVoteMaxIndexMaxTermProof.v
index 36b7985..6cc7849 100644
--- a/raft-proofs/RequestVoteMaxIndexMaxTermProof.v
+++ b/raft-proofs/RequestVoteMaxIndexMaxTermProof.v
@@ -3,7 +3,7 @@ From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import RequestVoteMaxIndexMaxTermInterface.
 From VerdiRaft Require Import RequestVoteTermSanityInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section RequestVoteMaxIndexMaxTerm.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/RequestVoteReplyMoreUpToDateProof.v b/raft-proofs/RequestVoteReplyMoreUpToDateProof.v
index b362f7d..9119d27 100644
--- a/raft-proofs/RequestVoteReplyMoreUpToDateProof.v
+++ b/raft-proofs/RequestVoteReplyMoreUpToDateProof.v
@@ -5,7 +5,7 @@ From VerdiRaft Require Import RequestVoteReplyTermSanityInterface.
 From VerdiRaft Require Import VotedForMoreUpToDateInterface.
 From VerdiRaft Require Import RequestVoteReplyMoreUpToDateInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section RequestVoteReplyMoreUpToDate.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/RequestVoteReplyTermSanityProof.v b/raft-proofs/RequestVoteReplyTermSanityProof.v
index 9112892..dc688eb 100644
--- a/raft-proofs/RequestVoteReplyTermSanityProof.v
+++ b/raft-proofs/RequestVoteReplyTermSanityProof.v
@@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface.
 From VerdiRaft Require Import SpecLemmas RequestVoteTermSanityInterface.
 From VerdiRaft Require Import RequestVoteReplyTermSanityInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section RequestVoteReplyTermSanity.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/RequestVoteTermSanityProof.v b/raft-proofs/RequestVoteTermSanityProof.v
index ac1922f..cc095f3 100644
--- a/raft-proofs/RequestVoteTermSanityProof.v
+++ b/raft-proofs/RequestVoteTermSanityProof.v
@@ -1,7 +1,7 @@
 From VerdiRaft Require Import Raft RaftRefinementInterface.
 From VerdiRaft Require Import SpecLemmas RequestVoteTermSanityInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section RequestVoteTermSanity.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/StateMachineCorrectProof.v b/raft-proofs/StateMachineCorrectProof.v
index c46c8b8..b7042c3 100644
--- a/raft-proofs/StateMachineCorrectProof.v
+++ b/raft-proofs/StateMachineCorrectProof.v
@@ -6,7 +6,7 @@ From VerdiRaft Require Import LogMatchingInterface.
 From VerdiRaft Require Import StateMachineCorrectInterface.
 From Coq Require Import ZArith.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section StateMachineCorrect.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/StateMachineSafetyPrimeProof.v b/raft-proofs/StateMachineSafetyPrimeProof.v
index ad05c63..fff41b6 100644
--- a/raft-proofs/StateMachineSafetyPrimeProof.v
+++ b/raft-proofs/StateMachineSafetyPrimeProof.v
@@ -14,7 +14,7 @@ From VerdiRaft Require Import LogsLeaderLogsInterface.
 From VerdiRaft Require Import OneLeaderLogPerTermInterface.
 From VerdiRaft Require Import RefinedLogMatchingLemmasInterface.
 
-Local Arguments update {_} {_} {_} _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} {_} _ _ _ _ : simpl never.
 
 Section StateMachineSafety'.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/StateMachineSafetyProof.v b/raft-proofs/StateMachineSafetyProof.v
index aadbe94..fe763b5 100644
--- a/raft-proofs/StateMachineSafetyProof.v
+++ b/raft-proofs/StateMachineSafetyProof.v
@@ -24,7 +24,7 @@ From VerdiRaft Require Import RefinedLogMatchingLemmasInterface.
 From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import RaftMsgRefinementInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section StateMachineSafetyProof.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/TermsAndIndicesFromOneLogProof.v b/raft-proofs/TermsAndIndicesFromOneLogProof.v
index 54b605e..a249ed5 100644
--- a/raft-proofs/TermsAndIndicesFromOneLogProof.v
+++ b/raft-proofs/TermsAndIndicesFromOneLogProof.v
@@ -1,16 +1,14 @@
-Require Import VerdiRaft.Raft.
-Require Import VerdiRaft.CommonTheorems.
-Require Import VerdiRaft.SpecLemmas.
+From VerdiRaft Require Import Raft CommonTheorems SpecLemmas.
+From VerdiRaft Require Import TermsAndIndicesFromOneLogInterface.
+From VerdiRaft Require Import CurrentTermGtZeroInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
-
-Require Import VerdiRaft.TermsAndIndicesFromOneLogInterface.
-Require Import VerdiRaft.CurrentTermGtZeroInterface.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section TermsAndIndicesFromOneLog.
   Context {orig_base_params : BaseParams}.
   Context {one_node_params : OneNodeParams orig_base_params}.
   Context {raft_params : RaftParams orig_base_params}.
+
   Context {ctgzi : current_term_gt_zero_interface}.
 
   Definition terms_and_indices_from_one_log_ind (net : network) : Prop :=
diff --git a/raft-proofs/TermsAndIndicesFromOneProof.v b/raft-proofs/TermsAndIndicesFromOneProof.v
index 8d61a56..053d828 100644
--- a/raft-proofs/TermsAndIndicesFromOneProof.v
+++ b/raft-proofs/TermsAndIndicesFromOneProof.v
@@ -1,13 +1,10 @@
-Require Import VerdiRaft.Raft.
-Require Import VerdiRaft.RaftRefinementInterface.
-Require Import VerdiRaft.CommonDefinitions.
-Require Import VerdiRaft.SpecLemmas.
-Require Import VerdiRaft.RefinementSpecLemmas.
+From VerdiRaft Require Import Raft RaftRefinementInterface.
+From VerdiRaft Require Import CommonDefinitions SpecLemmas.
+From VerdiRaft Require Import RefinementSpecLemmas.
+From VerdiRaft Require Import TermsAndIndicesFromOneInterface.
+From VerdiRaft Require Import TermsAndIndicesFromOneLogInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
-
-Require Import VerdiRaft.TermsAndIndicesFromOneInterface.
-Require Import VerdiRaft.TermsAndIndicesFromOneLogInterface.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section TermsAndIndicesFromOne.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/VotedForMoreUpToDateProof.v b/raft-proofs/VotedForMoreUpToDateProof.v
index 38e19ef..a762731 100644
--- a/raft-proofs/VotedForMoreUpToDateProof.v
+++ b/raft-proofs/VotedForMoreUpToDateProof.v
@@ -4,7 +4,7 @@ From VerdiRaft Require Import RequestVoteMaxIndexMaxTermInterface.
 From VerdiRaft Require Import VotedForTermSanityInterface.
 From VerdiRaft Require Import VotedForMoreUpToDateInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section VotedForMoreUpToDate.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/VotedForTermSanityProof.v b/raft-proofs/VotedForTermSanityProof.v
index 98b3229..e1151cb 100644
--- a/raft-proofs/VotedForTermSanityProof.v
+++ b/raft-proofs/VotedForTermSanityProof.v
@@ -3,7 +3,7 @@ From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import RequestVoteTermSanityInterface.
 From VerdiRaft Require Import VotedForTermSanityInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section VotedForTermSanity.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/VotesCorrectProof.v b/raft-proofs/VotesCorrectProof.v
index e1004dd..1e932d7 100644
--- a/raft-proofs/VotesCorrectProof.v
+++ b/raft-proofs/VotesCorrectProof.v
@@ -3,7 +3,7 @@ From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import VotesCorrectInterface.
 From VerdiRaft Require Import VotesLeCurrentTermInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section VotesCorrect.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/VotesLeCurrentTermProof.v b/raft-proofs/VotesLeCurrentTermProof.v
index 0ba7413..71c7896 100644
--- a/raft-proofs/VotesLeCurrentTermProof.v
+++ b/raft-proofs/VotesLeCurrentTermProof.v
@@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface.
 From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import VotesLeCurrentTermInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section VotesLeCurrentTerm.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/VotesReceivedMoreUpToDateProof.v b/raft-proofs/VotesReceivedMoreUpToDateProof.v
index 42511f8..05b82a8 100644
--- a/raft-proofs/VotesReceivedMoreUpToDateProof.v
+++ b/raft-proofs/VotesReceivedMoreUpToDateProof.v
@@ -3,7 +3,7 @@ From VerdiRaft Require Import RefinementSpecLemmas CommonTheorems.
 From VerdiRaft Require Import RequestVoteReplyMoreUpToDateInterface.
 From VerdiRaft Require Import VotesReceivedMoreUpToDateInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section VotesReceivedMoreUpToDate.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/VotesVotesWithLogCorrespondProof.v b/raft-proofs/VotesVotesWithLogCorrespondProof.v
index 099313c..26d4a85 100644
--- a/raft-proofs/VotesVotesWithLogCorrespondProof.v
+++ b/raft-proofs/VotesVotesWithLogCorrespondProof.v
@@ -1,7 +1,7 @@
 From VerdiRaft Require Import Raft RaftRefinementInterface.
 From VerdiRaft Require Import VotesVotesWithLogCorrespondInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section VotesVotesWithLogCorrespond.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/VotesWithLogSortedProof.v b/raft-proofs/VotesWithLogSortedProof.v
index 07489ab..74ac0d2 100644
--- a/raft-proofs/VotesWithLogSortedProof.v
+++ b/raft-proofs/VotesWithLogSortedProof.v
@@ -4,7 +4,7 @@ From VerdiRaft Require Import CommonDefinitions SpecLemmas.
 From VerdiRaft Require Import VotesWithLogSortedInterface.
 From VerdiRaft Require Import SortedInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section VotesWithLogSorted.
   Context {orig_base_params : BaseParams}.
diff --git a/raft-proofs/VotesWithLogTermSanityProof.v b/raft-proofs/VotesWithLogTermSanityProof.v
index 987899e..3d4b59c 100644
--- a/raft-proofs/VotesWithLogTermSanityProof.v
+++ b/raft-proofs/VotesWithLogTermSanityProof.v
@@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface.
 From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas.
 From VerdiRaft Require Import VotesWithLogTermSanityInterface.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section VotesWithLogTermSanity.
 
diff --git a/raft/AppendEntriesRequestsCameFromLeadersInterface.v b/raft/AppendEntriesRequestsCameFromLeadersInterface.v
index dadb693..9433b9d 100644
--- a/raft/AppendEntriesRequestsCameFromLeadersInterface.v
+++ b/raft/AppendEntriesRequestsCameFromLeadersInterface.v
@@ -1,5 +1,4 @@
-Require Import VerdiRaft.Raft.
-Require Import VerdiRaft.RaftRefinementInterface.
+From VerdiRaft Require Import Raft RaftRefinementInterface.
 
 Section AppendEntriesRequestsCameFromLeaders.
   Context {orig_base_params : BaseParams}.
diff --git a/raft/CommonTheorems.v b/raft/CommonTheorems.v
index 6c40825..850e6c9 100644
--- a/raft/CommonTheorems.v
+++ b/raft/CommonTheorems.v
@@ -2,7 +2,7 @@ From Coq Require Import PeanoNat FunInd.
 From VerdiRaft Require Import RaftState Raft.
 From VerdiRaft Require Export CommonDefinitions.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section CommonTheorems.
   Context {orig_base_params : BaseParams}.
diff --git a/raft/RefinementCommonTheorems.v b/raft/RefinementCommonTheorems.v
index c49f48b..247af70 100644
--- a/raft/RefinementCommonTheorems.v
+++ b/raft/RefinementCommonTheorems.v
@@ -6,7 +6,7 @@ From VerdiRaft Require Import CommonTheorems.
 From VerdiRaft Require Export RefinementCommonDefinitions.
 From VerdiRaft Require Import SpecLemmas.
 
-Local Arguments update {_} {_} _ _ _ _ _ : simpl never.
+#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never.
 
 Section CommonTheorems.
   Context {orig_base_params : BaseParams}.
diff --git a/raft/TermsAndIndicesFromOneInterface.v b/raft/TermsAndIndicesFromOneInterface.v
index 6807348..4bf7f00 100644
--- a/raft/TermsAndIndicesFromOneInterface.v
+++ b/raft/TermsAndIndicesFromOneInterface.v
@@ -1,6 +1,5 @@
-Require Import VerdiRaft.Raft.
-Require Import VerdiRaft.RaftRefinementInterface.
-Require Import VerdiRaft.CommonDefinitions.
+From VerdiRaft Require Import Raft RaftRefinementInterface.
+From VerdiRaft Require Import CommonDefinitions.
 
 Section TermsAndIndicesFromOne.
   Context {orig_base_params : BaseParams}.
diff --git a/raft/TermsAndIndicesFromOneLogInterface.v b/raft/TermsAndIndicesFromOneLogInterface.v
index 820f645..936847d 100644
--- a/raft/TermsAndIndicesFromOneLogInterface.v
+++ b/raft/TermsAndIndicesFromOneLogInterface.v
@@ -1,6 +1,4 @@
-Require Import VerdiRaft.Raft.
-
-Require Import VerdiRaft.CommonDefinitions.
+From VerdiRaft Require Import Raft CommonDefinitions.
 
 Section TermsAndIndicesFromOneLogInterface.
   Context {orig_base_params : BaseParams}.
diff --git a/systems/VarDRaftSerializers.v b/systems/VarDRaftSerializers.v
index e81388e..dae3996 100644
--- a/systems/VarDRaftSerializers.v
+++ b/systems/VarDRaftSerializers.v
@@ -161,7 +161,7 @@ Section Serializers.
       cheerios_crush.
   Qed.
 
-  Global Instance msg_Serializer : Serializer msg :=
+  #[global] Instance msg_Serializer : Serializer msg :=
     {| serialize := msg_serialize;
        deserialize := msg_deserialize;
        serialize_deserialize_id := msg_serialize_deserialize_id |}.
@@ -217,7 +217,7 @@ Section Serializers.
       repeat (cheerios_crush; simpl).
   Qed.
 
-  Global Instance output_Serializer : Serializer output :=
+  #[global] Instance output_Serializer : Serializer output :=
     {| serialize := serialize_output;
        deserialize := deserialize_output;
        serialize_deserialize_id := output_serialize_deserialize_id |}.
@@ -265,7 +265,7 @@ Section Serializers.
     reflexivity.
   Qed.
 
-  Global Instance raft_data_Serializer : Serializer raft_data :=
+  #[global] Instance raft_data_Serializer : Serializer raft_data :=
     {| serialize := serialize_raft_data;
        deserialize := deserialize_raft_data;
        serialize_deserialize_id := raft_data_serialize_deserialize_id |}.
@@ -302,7 +302,7 @@ Section Serializers.
     destruct i; repeat (cheerios_crush; simpl).
   Qed.
 
-  Global Instance raft_input_Serializer : Serializer raft_input :=
+  #[global] Instance raft_input_Serializer : Serializer raft_input :=
     {| serialize := serialize_raft_input;
        deserialize := deserialize_raft_input;
        serialize_deserialize_id := raft_input_serialize_deserialize_id |}.