Merge pull request #33 from coq-community/coq_17484

Adapt to coq/coq#17484
coq-community · Jul 8, 2023 · f710b62 · f710b62
2 parents e29827f + cf8d2bb
commit f710b62
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? *)