adapt to coq/coq#19872 (Inductive ": Type" means Type)

mit-plv · Nov 25, 2024 · 433e912 · 433e912
1 parent 40b6953
commit 433e912
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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