From 27021cf76669acdbd6c8fb566355c672fedf783c Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 11 May 2021 16:25:49 +0900
Subject: [PATCH] to avoid clash with ssrbool.symmetric

---
 CHANGELOG_UNRELEASED.md | 2 ++
 theories/forms.v        | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 5e316b600..83f79505d 100644
--- 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
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.