diff options
| author | Amin Timany | 2017-05-05 13:33:18 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-16 04:51:18 +0200 |
| commit | 7b323421ba558011c304a686c4cd368e1ff39440 (patch) | |
| tree | d83baa256f9794e2281dd710972efaf2e7f73da6 | |
| parent | 0c94de1f8c598c1869f71fee86bdbe4f0000a502 (diff) | |
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.
| -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 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 } |