Merge pull request #379 from math-comp/forms_20210511

minor adjustements to `forms.v`
math-comp · Jun 1, 2021 · 49417f1 · 49417f1
2 parents 7c0d18c + 27021cf
commit 49417f1
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git 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
@@ -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.