From 2bb2877795ca1b6234dae05fe9b55e68abcd22ea Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Fri, 18 Aug 2017 15:35:33 +0200
Subject: Correct the option for cumulativity in CHANGES

---
 CHANGES | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index ed2f17206..a54e8a426 100644
--- a/CHANGES
+++ b/CHANGES
@@ -156,7 +156,7 @@ Build Infrastructure
 Universes
 
 - Cumulative inductive types. see prefixes "Cumulative", "NonCumulative"
-  for inductive definitions and the option "Set Inductive Cumulativity"
+  for inductive definitions and the option "Set Polymorphic Inductive Cumulativity"
   in the reference manual.
 - New syntax `foo@{_}` to instantiate a polymorphic definition with
   anonymous universes (can also be used with `Type`).
-- 
cgit v1.2.3