analysis icon indicating copy to clipboard operation
analysis copied to clipboard

lebesgue_integral file incompatible with fingroup

Open CohenCyril opened this issue 1 year ago • 0 comments

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.

CohenCyril avatar Oct 22 '24 07:10 CohenCyril