analysis
analysis copied to clipboard
forms incompatible with mathcomp-character
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.