Adapt to coq/coq#17484

coq-community · Jul 8, 2023 · cf8d2bb · cf8d2bb
1 parent e29827f
commit cf8d2bb
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/core/transfer.v b/theories/core/transfer.v
@@ -567,7 +567,7 @@ Proof.
   - rewrite /vfun_of/= vfun_bodyE. exact: inj_v_open.
     move => H /=. by rewrite imfset_bij_bwdE.
   - rewrite /vfun_of/= vfun_bodyE. exact: inj_v_open.
-    move => H /=. by rewrite imfset_bij_bwdE //=.
+    move => H /=. by rewrite imfset_bij_bwdE.
 Qed.
 
 (* This follows the same pattern as open_add_vertex. Lemma? *)