From 64ea715e48b14ec8a793453b76db332e032d5cb0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 18 Jan 2020 11:51:48 +0100
Subject: Reference manual: Typos/English in chapter universe polymorphism.

---
 doc/sphinx/addendum/universe-polymorphism.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index 7adb25cbd6..f9cc25959c 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -529,8 +529,8 @@ sections, except in the following ways:
        Polymorphic Universe i.
        Fail Constraint i = i.
 
-  This includes constraints implictly declared by commands such as
-  :cmd:`Variable`, which may as a such need to be used with universe
+  This includes constraints implicitly declared by commands such as
+  :cmd:`Variable`, which may need to be used with universe
   polymorphism activated (locally by attribute or globally by option):
 
   .. coqtop:: all
-- 
cgit v1.2.3