From a9f50489677c4c803a040a0ab61274bdee39218c Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 12 May 2021 11:59:21 +0200
Subject: [PATCH] Make more uniform Arguments for type fields.

---
 theories/typing/type.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/typing/type.v b/theories/typing/type.v
index 2cecc1eb..627b5111 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -51,7 +51,9 @@ Instance: Params (@ty_size) 2 := {}.
 Instance: Params (@ty_own) 2 := {}.
 Instance: Params (@ty_shr) 2 := {}.
 
-Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
+Arguments ty_size {_ _} _ / : simpl nomatch.
+Arguments ty_own {_ _} _ _ _ / : simpl nomatch.
+Arguments ty_shr {_ _} _ _ _ _ / : simpl nomatch.
 
 Class TyWf `{!typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
 Arguments ty_lfts {_ _} _ {_}.
-- 
GitLab