From 5aef9a66966c8aa97041461d618b601e60e56c91 Mon Sep 17 00:00:00 2001
From: Rutger Broekhoff
Date: Thu, 27 Jun 2024 02:13:26 +0200
Subject: Be consistent in notation of simplify_eq/=

---
 semprop.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'semprop.v')

diff --git a/semprop.v b/semprop.v
index 2fe30af..7ab0707 100644
--- a/semprop.v
+++ b/semprop.v
@@ -42,7 +42,7 @@ Proof.
   - exfalso. apply H. by exists bs.
   - f_equal. by eapply matches_deterministic.
   - apply map_insert_inv in H0 as [H01 H02].
-    by simplify_eq /=.
+    by simplify_eq/=.
   - f_equal. by eapply binop_deterministic.
   - rewrite H4 in H. by apply is_Some_None in H.
   - exfalso. apply H4. by exists bs.
-- 
cgit v1.2.3