From 5e156c9bd37e89762cf61630fe4f01008a94bfa8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Aug 2024 09:58:56 +0200
Subject: [PATCH] Forward compatibility fixes for
 https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/555

---
 gpfsl-examples/list_helper.v | 2 +-
 gpfsl/lang/lang.v            | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/gpfsl-examples/list_helper.v b/gpfsl-examples/list_helper.v
index 3c7ea936..2f5e09ca 100644
--- a/gpfsl-examples/list_helper.v
+++ b/gpfsl-examples/list_helper.v
@@ -45,7 +45,7 @@ Proof. apply prefix_app_inv. Qed.
 End prefixes.
 
 Global Instance fmap_prefix {A B} (f : A → B) :
-  Proper ((⊑) ==> (⊑)) (@fmap list _ _ _ f).
+  Proper ((⊑@{list _}) ==> (⊑)) (fmap f).
 Proof. intros L1 L2 [L3 Eq3]. rewrite Eq3. rewrite fmap_app. by eexists. Qed.
 
 Lemma lookup_fmap_Some' `{FinMap K M} {A B} (f : A → B) (m : M A) i y :
diff --git a/gpfsl/lang/lang.v b/gpfsl/lang/lang.v
index ec4dfeac..c7125e81 100644
--- a/gpfsl/lang/lang.v
+++ b/gpfsl/lang/lang.v
@@ -653,8 +653,8 @@ Module base.
        | _ => Lit LitPoison
        end) _).
     fix FIX 1. intros []; f_equal=>//; revert select (list expr); clear -FIX.
-    - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
-    - fix FIX_INNER 1. intros []; [done|]. by simpl; f_equal.
+    - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
+    - fix FIX_INNER 1. intros []; [done|]. by f_equal/=.
   Qed.
 
   Global Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
-- 
GitLab