From 850a722b406d478ea165f9f212642f6e3045cc4b Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> Date: Wed, 12 May 2021 13:29:37 +0200 Subject: [PATCH] Revert "Uniform Arguments for simple_type" This reverts commit f4a6ea09f99499f974e011bbe114287fcc034317. --- theories/typing/type.v | 2 -- 1 file changed, 2 deletions(-) diff --git a/theories/typing/type.v b/theories/typing/type.v index 0a67e7f2..61c8cf75 100644 --- a/theories/typing/type.v +++ b/theories/typing/type.v @@ -121,8 +121,6 @@ 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