fix

affeldt-aist · Apr 25, 2024 · 2b07fac · 2b07fac
1 parent dee2ea6
commit 2b07fac
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/probability/convex.v b/probability/convex.v
@@ -1944,10 +1944,11 @@ Import LmoduleConvex.
 Let linear_is_affine: affine f.
 Proof. by move=>p x y; rewrite linearD 2!linearZZ. Qed.
 
-#[non_forgetful_inheritance] HB.instance Definition _ := isAffine.Build _ _ _ linear_is_affine.
+#[export] HB.instance Definition _ := isAffine.Build _ _ _ linear_is_affine.
 
 End linear_affine.
 End LinearAffine.
+HB.export LinearAffine.
 
 (* TOTHINK: Should we keep this section, only define R_convType, or something else ? *)
 Module RConvex.