diff --git a/HB/common/utils-synterp.elpi b/HB/common/utils-synterp.elpi
index 73932c1a..82962ad8 100644
--- a/HB/common/utils-synterp.elpi
+++ b/HB/common/utils-synterp.elpi
@@ -24,6 +24,7 @@ with-attributes P :-
     att "primitive" bool,
     att "non_forgetful_inheritance" bool,
     att "hnf" bool,
+	 att "typeclass" bool,
   ] Opts, !,
   Opts => (save-docstring, P).
 
diff --git a/tests/coercion.v b/tests/coercion.v
index 6918fed5..6eaf1e87 100644
--- a/tests/coercion.v
+++ b/tests/coercion.v
@@ -5,7 +5,7 @@ HB.mixin Record isSigma (T : Type) (P : T -> Prop) (x : T) := {
   _ : P x
 }.
 
-#[short(type="sigType"), verbose]
+#[short(type="sigType"), typeclass]
 HB.structure Definition Sig (T : Type) (P : T -> Prop) := {x of isSigma T P x}.
 
 Section Sigma.
@@ -45,7 +45,7 @@ Fail Check x : sigType A P.
 End Sigma.
 
 HB.mixin Record isSigmaT (P : Type -> Prop) (x : Type) := { _ : P x }.
-#[short(type="sigTType"), verbose]
+#[short(type="sigTType"), typeclass]
 HB.structure Definition SigT (P : Type -> Prop) := {x of isSigmaT P x}.
 
 Section SigmaT.