Hello,Perhaps I'm overlooking something but replacing include BIwith include (BI : B with type t := t)seems like a reasonable fix to me.Danny