more on commutator subgroups · HoTT/Coq-HoTT@b589965

Build HoTT: theories/Algebra/Groups/Subgroup.v#L228

Expected a single focused goal but 6 goals are focused.

Build HoTT: theories/Algebra/Groups/FreeProduct.v#L522

Cannot infer this placeholder of type

Build HoTT: theories/Basics/Notations.v#L13

Set ... Append is not supported.

Build HoTT: theories/Basics/Notations.v#L13

Set ... Append is not supported.

Build HoTT: theories/Basics/Settings.v#L10

"coq-core" has been renamed to "rocq-runtime".

Build HoTT: theories/Basics/Settings.v#L12

"coq-core" has been renamed to "rocq-runtime".

Build HoTT: theories/Categories/Category/Pi.v#L48

Set ... Append is not supported.

Build HoTT: theories/Categories/Category/Pi.v#L48

Set ... Append is not supported.

Build HoTT: theories/Categories/Functor/Prod/Core.v#L106

Set ... Append is not supported.

Build HoTT: theories/Categories/Functor/Prod/Core.v#L106

Set ... Append is not supported.

Build HoTT: theories/Categories/Comma/Core.v#L342

Set ... Append is not supported.

Build HoTT: theories/Categories/Comma/Core.v#L342

Set ... Append is not supported.

Provide feedback