Extra parentheses needed in argument of a prefix notation at level 0.

jwiegley · Oct 29, 2023 · 01f334c · 01f334c
1 parent 3edcc3a
commit 01f334c
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Instance/Cones/Limit.v b/Instance/Cones/Limit.v
@@ -11,7 +11,7 @@ Program Definition Limit_Cones `(F : J ⟶ C) `{T : @Terminal (Cones F)} :
   Limit F := {|
   limit_cone := @terminal_obj _ T;
   ump_limits := fun N =>
-    {| unique_obj := `1 @one _ T N
-     ; unique_property := `2 @one _ T N
+    {| unique_obj := `1 (@one _ T N)
+     ; unique_property := `2 (@one _ T N)
      ; uniqueness       := fun v H => @one_unique _ T N (@one _ T N) (v; H) |}
 |}.