aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rtrigo.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/Rtrigo.v')
-rw-r--r--theories/Reals/Rtrigo.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 335728b2b..f8db0463f 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -1704,4 +1704,4 @@ Lemma cos_eq_0_2PI_1 :
intros x H1 H2 H3; elim H3; intro H4;
[ rewrite H4; rewrite cos_PI2; reflexivity
| rewrite H4; rewrite cos_3PI2; reflexivity ].
-Qed. \ No newline at end of file
+Qed.