Adapt to math-comp/math-comp#1133 (replace fun_scope with function_scope) · coq-community/bits@20c8d28

Notation "[ finType of _ ]" is deprecated since mathcomp 2.0.0.

Ignoring canonical projection to isCountable.pickleK by

Ignoring canonical projection to isCountable.unpickle by

Ignoring canonical projection to isCountable.pickle by

Ignoring canonical projection to inj_eqAxiom by hasDecEq.eqP in

Ignoring canonical projection to eq_op by hasDecEq.eq_op in

Ignoring canonical projection to FinTuple.enumP by

Ignoring canonical projection to FinTuple.enum by

Ignoring canonical projection to GRing.isZmodule.addNr by

Ignoring canonical projection to GRing.isZmodule.opp by

Provide feedback