analysis
analysis copied to clipboard
lebesgue_integral file incompatible with fingroup
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import all_fingroup.
From mathcomp Require Import lebesgue_integral.
fails with error
Error: Notation "_ \x _" is already defined at level 40 with arguments constr
at level 40, constr at next level while it is now required to be at level 40
with arguments constr at next level, constr at next level.
Notation "_ \x _" must be reused as was.