fix test

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Jul 4, 2024 · 4c82e00 · 4c82e00
1 parent f02879a
commit 4c82e00
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/test/WildCat/Opposite.v b/test/WildCat/Opposite.v
@@ -68,5 +68,5 @@ Fail Definition test A `{HasEquivs A}
 (** Opposite braidings are definitionally involutive. *)
 Succeed Definition test A `{HasEquivs A}
   (F : A -> A -> A) `{!Is0Bifunctor F, !Is1Bifunctor F} (a : Braiding F)
-  : @braiding_op _ _ _ _ _ _ _ _ (@braiding_op _ _ _ _ _ _ _ _ a) = a
+  : @braiding_op _ _ _ _ _ _ _ _ _ (@braiding_op _ _ _ _ _ _ _ _ _ a) = a
   := 1.