From 7b323421ba558011c304a686c4cd368e1ff39440 Mon Sep 17 00:00:00 2001
From: Amin Timany
Date: Fri, 5 May 2017 13:33:18 +0200
Subject: Change the option to Set Inductive Cumulativity

This requires to change the status of Inductive (we have also changed
CoInductive and Variant) from keyword to identifier.
---
 test-suite/coqchk/cumulativity.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/coqchk/cumulativity.v b/test-suite/coqchk/cumulativity.v
index 5d245aaa5d..3a8f9fa22f 100644
--- a/test-suite/coqchk/cumulativity.v
+++ b/test-suite/coqchk/cumulativity.v
@@ -1,5 +1,5 @@
 Set Universe Polymorphism.
-Set Ind Cumulativity.
+Set Inductive Cumulativity.
 Set Printing Universes.
 
 Inductive List (A: Type) := nil | cons : A -> List A -> List A.
-- 
cgit v1.2.3