fixed syntax

imdea-software · Jan 15, 2025 · d9079c3 · d9079c3
1 parent 19aa505
commit d9079c3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/pcm/unionmap.v b/pcm/unionmap.v
@@ -444,7 +444,7 @@ have [k H3] : exists k, k \in supp fx.
 - case: (supp fx) {E1 E} E2=>[|k s _] //.
   by exists k; rewrite inE eqxx. 
 suff : k \in supp (fcat fx fy) by rewrite E1. 
-by rewrite supp_fcat inE H3.
+by rewrite supp_fcat inE /= H3.
 Qed.
 
 HB.instance Definition _ := isPCMC.Build T union_map_is_conical.