From 433e91211a333e73566b0eaa4da1a7d12ed972aa Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Mon, 25 Nov 2024 18:33:31 +0000
Subject: [PATCH] adapt to coq/coq#19872 (Inductive ": Type" means Type)

---
 src/grw.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/grw.v b/src/grw.v
index 3f999db..9f496d7 100644
--- a/src/grw.v
+++ b/src/grw.v
@@ -2709,7 +2709,7 @@ Module LanguageImpl.
                  (@Mbind_Mret_r)
                  (@Mbind_comm).
 
-  Inductive const : Type :=
+  Inductive const : Set :=
   | coin.
   Definition const_eqb (c1 c2 : const) : bool :=
     match c1, c2 with