aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorthery2019-03-29 15:31:54 +0100
committerthery2019-03-29 15:31:54 +0100
commit8f86085a1761153ab97f896a67fa9ffa9f139b78 (patch)
tree8ab526e3290dbe8dc52ac26b0e52ad1e51e01a71
parent4b9636ffd47ea5a0b99df442047ba03d18422738 (diff)
typo in ring.rst
-rw-r--r--doc/sphinx/addendum/ring.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst
index 20e4c6a3d6..3b350d5dc0 100644
--- a/doc/sphinx/addendum/ring.rst
+++ b/doc/sphinx/addendum/ring.rst
@@ -323,7 +323,7 @@ The syntax for adding a new ring is
decidable :n:`@term`
declares the ring as computational. The expression
:n:`@term` is the correctness proof of an equality test ``?=!``
- (which hould be evaluable). Its type should be of the form
+ (which should be evaluable). Its type should be of the form
``forall x y, x ?=! y = true → x == y``.
morphism :n:`@term`