From 8f86085a1761153ab97f896a67fa9ffa9f139b78 Mon Sep 17 00:00:00 2001
From: thery
Date: Fri, 29 Mar 2019 15:31:54 +0100
Subject: typo in ring.rst

---
 doc/sphinx/addendum/ring.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc')

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`
-- 
cgit v1.2.3