From 7c82718f18afa3b317873f756a8801774ef64061 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 9 Oct 2015 13:19:20 +0200
Subject: Minor typo in universe polymorphism doc.

---
 dev/doc/univpoly.txt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/doc/univpoly.txt b/dev/doc/univpoly.txt
index bad2ae36eb..9e243eead5 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -82,7 +82,7 @@ show that A's type is in cumululativity relation with id's type
 argument, incurring a universe constraint. To do this, one can simply
 call Typing.resolve_evars env evdref c which will do some infer_conv to
 produce the right constraints and put them in the evar_map. Of course in
-some cases you might now from an invariant that no new constraint would
+some cases you might know from an invariant that no new constraint would
 be produced and get rid of it. Anyway the kernel will tell you if you
 forgot some. As a temporary way out, [Universes.constr_of_global] allows
 you to make a constr from any non-polymorphic constant, but it will fail
-- 
cgit v1.2.3