Forward compatibility fixes for stdpp!555

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 :

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).