typeclass option for HB.structure

math-comp · Jun 27, 2024 · 19216eb · 19216eb
1 parent 9e09df7
commit 19216eb
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git 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
@@ -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.