consistently use annotations

uwplse · Oct 21, 2023 · 5cd40c1 · 5cd40c1
1 parent e6d042f
commit 5cd40c1
Show file tree

Hide file tree

Showing 75 changed files with 88 additions and 97 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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}.