type inference is a sharp weapon

it "infers" indexes (in the wrong place)

Author: gares

tests/subtype.v

@@ -22,7 +22,7 @@ SubK : forall x Px, val (@Sub x Px) = x
 
 HB.structure Definition SUB (T : Type) (P : pred T) := { S of is_SUB T P S }.
 
-HB.structure Definition SubInhab T P := { sT of is_inhab T & is_SUB T P sT }.
+HB.structure Definition SubInhab (T : Type) P := { sT of is_inhab T & is_SUB T P sT }.
 
 HB.structure Definition SubNontrivial T P := { sT of is_nontrivial sT & is_SUB T P sT }.