From f4a6ea09f99499f974e011bbe114287fcc034317 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Wed, 12 May 2021 13:05:16 +0200
Subject: [PATCH] Uniform Arguments for simple_type

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

diff --git a/theories/typing/type.v b/theories/typing/type.v
index 61c8cf75..0a67e7f2 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -121,6 +121,8 @@ Record simple_type `{!typeG Σ} :=
 Existing Instance st_own_persistent.
 Instance: Params (@st_own) 2 := {}.
 
+Arguments st_own {_ _} _ / : simpl nomatch.
+
 Program Definition ty_of_st `{!typeG Σ} (st : simple_type) : type :=
   {| ty_size := 1; ty_own := st.(st_own);
      (* [st.(st_own) tid vl] needs to be outside of the fractured
-- 
GitLab