analysis icon indicating copy to clipboard operation
analysis copied to clipboard

forms incompatible with mathcomp-character

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 all_algebra.
From mathcomp Require Import all_solvable.
From mathcomp Require Import all_field.
From mathcomp Require Import all_character.
From mathcomp Require Import forms.

errors

Error: Notation "'e_ _" is already defined at level 8 with arguments constr
at level 2 while it is now required to be at level 3 with arguments constr
at next level.

CohenCyril avatar Oct 22 '24 07:10 CohenCyril