From 84e70d1e47a88635128f0790e8acdfa7800c79a1 Mon Sep 17 00:00:00 2001
From: Junyoung/Clare Jang <jjc9310@gmail.com>
Date: Mon, 22 Jan 2024 00:44:25 -0500
Subject: [PATCH] Make some contr args more implicit

---
 theories/Core/Semantic/PER.v | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/Core/Semantic/PER.v b/theories/Core/Semantic/PER.v
index df44adee..764d737c 100644
--- a/theories/Core/Semantic/PER.v
+++ b/theories/Core/Semantic/PER.v
@@ -39,17 +39,17 @@ Definition per_top_typ : relation domain := fun a b => (forall s, exists C, {{ R
 Inductive per_nat : relation domain :=
 | per_nat_zero : {{ Dom zero ≈ zero ∈ per_nat }}
 | per_nat_succ :
-  `( {{ Dom m ≈ n ∈ per_nat }} ->
-     {{ Dom succ m ≈ succ n ∈ per_nat }} )
+  `{ {{ Dom m ≈ n ∈ per_nat }} ->
+     {{ Dom succ m ≈ succ n ∈ per_nat }} }
 | per_nat_neut :
-  `( {{ Dom m ≈ n ∈ per_bot }} ->
-     {{ Dom ⇑ ℕ m ≈ ⇑ ℕ n ∈ per_nat }} )
+  `{ {{ Dom m ≈ n ∈ per_bot }} ->
+     {{ Dom ⇑ ℕ m ≈ ⇑ ℕ n ∈ per_nat }} }
 .
 
 Inductive per_ne : relation domain :=
 | per_ne_neut :
-  `( {{ Dom m ≈ n ∈ per_bot }} ->
-     {{ Dom ⇑ a m ≈ ⇑ a' n ∈ per_ne }} )
+  `{ {{ Dom m ≈ n ∈ per_bot }} ->
+     {{ Dom ⇑ a m ≈ ⇑ a' n ∈ per_ne }} }
 .
 
 Module Per_univ_def.