Merge pull request #155 from rmatthes/restorecompilationafterUniMathP…

…R1893 two adaptations to ArToSig now being defined through foldr1_map
UniMath · Jun 12, 2024 · e61c803 · e61c803
2 parents fb7ffc2 + 9ace96a
commit e61c803
Showing 1 changed file with 2 additions and 4 deletions.
diff --git a/Modules/Signatures/BindingSig.v b/Modules/Signatures/BindingSig.v
@@ -202,8 +202,7 @@ Section EpiSignatureSig.
       + intros n ar HI m epi_ar.
         intros M N f epif.
         unfold ArToSig,  Arity_to_Signature.
-        rewrite 2!map_cons.
-        rewrite foldr1_cons.
+        rewrite foldr1_map_cons.
         apply isEpi_binProdSig.
         * apply precompEpiFunc.
         * exact epi_ar.
@@ -224,8 +223,7 @@ Section EpiSignatureSig.
       + intros n ar HI m epi_ar.
         intros R epiR.
         unfold ArToSig,  Arity_to_Signature.
-        rewrite 2!map_cons.
-        rewrite foldr1_cons.
+        rewrite foldr1_map_cons.
         apply preserveEpi_binProdFunc.
         * apply productEpisSET.
         * apply precompEpiEpiFunc.