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/=

---
 maptools.v | 8 ++++----
 semprop.v  | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/maptools.v b/maptools.v
index ce4022a..01e24c0 100644
--- a/maptools.v
+++ b/maptools.v
@@ -9,7 +9,7 @@ Lemma map_insert_empty_lookup {A} `{FinMap K M}
 Proof.
   intros Hiel.
   destruct (decide (i = j)).
-  - split; try done. simplify_eq /=.
+  - split; try done. simplify_eq/=.
     rewrite lookup_insert in Hiel. congruence.
   - rewrite lookup_insert_ne in Hiel; try done.
     exfalso. eapply lookup_empty_Some, Hiel.
@@ -259,7 +259,7 @@ Proof.
   case_match.
   - case_match; try done.
     rewrite lookup_insert in H8. rewrite lookup_insert in H9.
-    simplify_eq /=. split; try done.
+    simplify_eq/=. split; try done.
     unfold map_Forall2, map_relation, option_relation.
     intros j.
     destruct (decide (i = j)).
@@ -275,7 +275,7 @@ Proof.
         case_match; case_match; try done;
           rewrite lookup_insert_ne in H11 by done;
           rewrite lookup_insert_ne in H12 by done;
-          by simplify_eq /=.
+          by simplify_eq/=.
   - by rewrite lookup_insert in H8.
 Qed.
 
@@ -305,7 +305,7 @@ Proof.
     pose proof (HForall2 i). by rewrite lookup_empty, lookup_insert in H15.
   - intros HForall2.
     apply map_Forall2_destruct in HForall2 as Hm2.
-    destruct Hm2 as [y [m2' [Hm21 Hm22]]]. simplify_eq /=.
+    destruct Hm2 as [y [m2' [Hm21 Hm22]]]. simplify_eq/=.
     apply map_Forall2_insert_inv_strict in HForall2 as [_ HForall2]; try done.
     set_solver.
 Qed.
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