adapt to coq#19822

mit-plv · Nov 18, 2024 · 98769a4 · 98769a4
1 parent dce6ce5
commit 98769a4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Common/FMapExtensions/LiftRelationInstances.v b/src/Common/FMapExtensions/LiftRelationInstances.v
@@ -84,7 +84,7 @@ Module FMapExtensionsLiftRelationInstances_fun (E: DecidableType) (Import M: WSf
           pose proof (R2_Reflexive default).
           t; compute in * |- ; split_and; break_match; try split;
             try solve [ eauto 3
-                      | eapply iffR_Proper; [ | | eauto ]; [ | eauto ]; eauto ].
+                      | eapply iffR_Proper; [ | | eapply R_Proper; eauto ]; eauto ].
         Qed.
 
         Global Instance lift_relation_gen_hetero_homo_Proper_Proper_subrelation