diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index d8affb61febe12f9787311586d6f228f6703d112..52246e1ab817df7c6e843bff863e753027491f10 100644
--- a/theories/examples/sort.v
+++ b/theories/examples/sort.v
@@ -51,7 +51,7 @@ Section sort.
 
   Definition sort_protocol_func : iProto Σ :=
     (<! A (I : A → val → iProp Σ) (R : A → A → Prop)
-         `{!RelDecision R, !Total R} (cmp : val)>
+         `(!RelDecision R, !Total R) (cmp : val)>
        MSG cmp {{ cmp_spec I R cmp }};
      sort_protocol I R)%proto.
 
diff --git a/theories/examples/sort_fg.v b/theories/examples/sort_fg.v
index f2ef96e9421cd608a97f8a95d912b0ce945f4ce4..5cd24e11acf889bc134b82919e07e1c20a2aa3e7 100644
--- a/theories/examples/sort_fg.v
+++ b/theories/examples/sort_fg.v
@@ -294,7 +294,7 @@ Section sort_fg.
 
   Definition sort_fg_func_protocol : iProto Σ :=
     (<! A (I : A → val → iProp Σ) (R : A → A → Prop)
-         `{!RelDecision R, !Total R} (cmp : val)>
+         `(!RelDecision R, !Total R) (cmp : val)>
        MSG cmp {{ cmp_spec I R cmp }};
      sort_fg_head_protocol I R [])%proto.
 
@@ -307,4 +307,4 @@ Section sort_fg.
     wp_recv (A I R ? ? cmp) as "#Hcmp".
     by wp_apply (sort_service_fg_spec with "Hcmp Hc").
   Qed.
-End sort_fg.
\ No newline at end of file
+End sort_fg.