Fix issue #789 (#807)

PrincetonUniversity · Jan 15, 2025 · ccb0df9 · ccb0df9
1 parent 21f3ac5
commit ccb0df9
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/floyd/functional_base.v b/floyd/functional_base.v
@@ -732,8 +732,8 @@ Qed.
 
 Lemma repr_inj_signed64:
   forall i j,
-    Int64.min_signed <= i <= Int.max_signed ->
-    Int64.min_signed <= j <= Int.max_signed ->
+    Int64.min_signed <= i <= Int64.max_signed ->
+    Int64.min_signed <= j <= Int64.max_signed ->
     Int64.repr i = Int64.repr j -> i=j.
 Proof.
 intros.