to avoid clash with ssrbool.symmetric

math-comp · Jun 1, 2021 · 27021cf · 27021cf
1 parent 09e03a7
commit 27021cf
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
@@ -135,6 +135,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.