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.
---
 parsing/g_vernac.ml4             | 6 +++---
 test-suite/coqchk/cumulativity.v | 2 +-
 vernac/vernacentries.ml          | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index e6b28b1d87..dbd2fc4016 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -232,9 +232,9 @@ GEXTEND Gram
 	r = universe_level -> (l, ord, r) ] ]
   ;
   finite_token:
-    [ [ "Inductive" -> (Inductive_kw,Finite)
-      | "CoInductive" -> (CoInductive,CoFinite)
-      | "Variant" -> (Variant,BiFinite)
+    [ [ IDENT "Inductive" -> (Inductive_kw,Finite)
+      | IDENT "CoInductive" -> (CoInductive,CoFinite)
+      | IDENT "Variant" -> (Variant,BiFinite)
       | IDENT "Record" -> (Record,BiFinite)
       | IDENT "Structure" -> (Structure,BiFinite)
       | IDENT "Class" -> (Class true,BiFinite) ] ]
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.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 580c81a0bd..957911e1e5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1368,7 +1368,7 @@ let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "inductive cumulativity";
-      optkey   = ["Ind"; "Cumulativity"];
+      optkey   = ["Inductive"; "Cumulativity"];
       optread  = Flags.is_inductive_cumulativity;
       optwrite = Flags.make_inductive_cumulativity }
 
-- 
cgit v1.2.3