From 86314340714364eeaa0771350f622bd4060a3427 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 4 Sep 2020 13:28:33 +0200
Subject: [PATCH] Bumped Coq 8.12 warning fixes

---
 theories/examples/sort.v    | 2 +-
 theories/examples/sort_fg.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/examples/sort.v b/theories/examples/sort.v
index d8affb6..52246e1 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 f2ef96e..5cd24e1 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.
-- 
GitLab