adapt to coq/coq#17937

mit-plv · Aug 24, 2023 · 1c6bef7 · 1c6bef7
1 parent 1ba5c2e
commit 1c6bef7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Rupicola/Lib/Core.v b/src/Rupicola/Lib/Core.v
@@ -1180,7 +1180,7 @@ Section Aliasing.
                 (truncated_word sz (mem := Mem)).
   Proof.
     red. intros * h Hmem.
-    pose proof bytes_per_range.
+    pose proof bytes_per_range sz.
     rewrite word.unsigned_of_Z_nowrap in h by lia.
     unfold scalar, truncated_word, truncated_scalar,
     littleendian, ptsto_bytes.ptsto_bytes in *.