From ccb0df9c251f1e6b61070d71752c5a7e213816d0 Mon Sep 17 00:00:00 2001
From: Andrew Appel <appel@princeton.edu>
Date: Wed, 15 Jan 2025 11:49:15 -0500
Subject: [PATCH] Fix issue #789 (#807)

---
 floyd/functional_base.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/floyd/functional_base.v b/floyd/functional_base.v
index 541017ca2..eb6689d51 100644
--- 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.