diff options
| -rw-r--r-- | parsing/g_vernac.ml4 | 6 | ||||
| -rw-r--r-- | test-suite/coqchk/cumulativity.v | 2 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index e6b28b1d8..dbd2fc401 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 5d245aaa5..3a8f9fa22 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 580c81a0b..957911e1e 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 } |