From 611da26d847888031cac4d6976b9e7e1e90cdc0e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 9 Dec 2017 23:14:19 +0100
Subject: [api] Remove yet another type alias.

---
 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 6a69c57934..ca3d520c70 100644
--- a/dev/doc/univpoly.txt
+++ b/dev/doc/univpoly.txt
@@ -12,7 +12,7 @@ type pinductive = inductive puniverses
 type pconstructor = constructor puniverses
 
 type constr = ...
-  | Const of puniversess
+  | Const of puniverses
   | Ind of pinductive
   | Constr of pconstructor
   | Proj of constant * constr
-- 
cgit v1.2.3