Top source

Module mathcomp.classical.mathcomp_extra

From mathcomp Require Import mathcomp_compat.

Attributes deprecated(since="mathcomp-analysis 1.18.0",
  note="use `mathcomp_compat.v` instead.").