aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/CyclicAxioms.v')
-rw-r--r--theories/Numbers/Cyclic/Abstract/CyclicAxioms.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
index 43aafe24b9..20016281a8 100644
--- a/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
+++ b/theories/Numbers/Cyclic/Abstract/CyclicAxioms.v
@@ -413,4 +413,4 @@ Qed.
Lemma eqb_correct : forall x y, eqb x y = true -> x==y.
Proof. now apply eqb_eq. Qed.
-End CyclicRing. \ No newline at end of file
+End CyclicRing.