aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--riscV/CSE2depsproof.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/riscV/CSE2depsproof.v b/riscV/CSE2depsproof.v
index 2ed12658..a3811e78 100644
--- a/riscV/CSE2depsproof.v
+++ b/riscV/CSE2depsproof.v
@@ -34,7 +34,7 @@ Section MEMORY_WRITE.
Variable chunkw chunkr : memory_chunk.
Variable base : val.
- Variable addrw addrr valw valr : val.
+ Variable addrw addrr valw : val.
Hypothesis STORE : Mem.storev chunkw m addrw valw = Some m2.
Section INDEXED_AWAY.