diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 269dedc6d..14136cdff 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -141,6 +141,8 @@ + `ge_Rfloor` -> `Rfloor_le` + `ler_floor` -> `floor_le` + `Rfloor_le` -> `le_Rfloor` +- in `forms.v`: + + `symmetric` -> `symmetric_form` ### Removed diff --git a/theories/forms.v b/theories/forms.v index fa472ef29..ce1f9e94a 100644 --- a/theories/forms.v +++ b/theories/forms.v @@ -485,7 +485,7 @@ End Sesquilinear. Notation "eps_theta .-sesqui" := (sesqui _ eps_theta) : ring_scope. -Notation symmetric := (false, [rmorphism of idfun]).-sesqui. +Notation symmetric_form := (false, [rmorphism of idfun]).-sesqui. Notation skew := (true, [rmorphism of idfun]).-sesqui. Notation hermitian := (false, @conjC _).-sesqui.