From 7865d0baf96ccbde37ed2f85e5ddbd5c24047eba Mon Sep 17 00:00:00 2001
From: Robert Rand
Date: Wed, 24 Jul 2019 14:33:42 -0400
Subject: changed name of cos3PI4 to cos_3PI4 for consistency

---
 theories/Reals/Rtrigo_calc.v | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/theories/Reals/Rtrigo_calc.v b/theories/Reals/Rtrigo_calc.v
index 5ed60b0a0f..2428fc495d 100644
--- a/theories/Reals/Rtrigo_calc.v
+++ b/theories/Reals/Rtrigo_calc.v
@@ -178,7 +178,7 @@ Proof.
   change (cos (PI / 4) <> 0); rewrite cos_PI4; apply R1_sqrt2_neq_0.
 Qed.
 
-Lemma cos3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2.
+Lemma cos_3PI4 : cos (3 * (PI / 4)) = -1 / sqrt 2.
 Proof.
   replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field.
   rewrite cos_shift; rewrite sin_neg; rewrite sin_PI4.
@@ -186,12 +186,16 @@ Proof.
   ring.
 Qed.
 
-Lemma sin3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2.
+#[deprecated(since="8.10",note="Use cos_3PI4 instead.")] Notation cos3PI4 := cos_3PI4.
+
+Lemma sin_3PI4 : sin (3 * (PI / 4)) = 1 / sqrt 2.
 Proof.
   replace (3 * (PI / 4)) with (PI / 2 - - (PI / 4)) by field.
   now rewrite sin_shift, cos_neg, cos_PI4.
 Qed.
 
+#[deprecated(since="8.10",note="Use sin_3PI4 instead.")] Notation sin3PI4 := sin_3PI4.
+
 Lemma cos_PI6 : cos (PI / 6) = sqrt 3 / 2.
 Proof with trivial.
   apply Rsqr_inj...
-- 
cgit v1.2.3