diff options
| author | Amin Timany | 2017-07-28 13:29:36 +0200 |
|---|---|---|
| committer | Amin Timany | 2017-07-31 18:05:54 +0200 |
| commit | 3b7e7f7738737475cb0f09130b0487c85906dd2b (patch) | |
| tree | 5e3990e47e793837f0ff2b6d7b87dba310ee535d /vernac | |
| parent | 28998d55aaaf0ad0e78477db5601a5bc9a6657b1 (diff) | |
Change the option for cumulativity
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3542c4081e..12a31953c5 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1369,10 +1369,10 @@ let _ = let _ = declare_bool_option { optdepr = false; - optname = "inductive cumulativity"; - optkey = ["Inductive"; "Cumulativity"]; - optread = Flags.is_inductive_cumulativity; - optwrite = Flags.make_inductive_cumulativity } + optname = "Polymorphic inductive cumulativity"; + optkey = ["Polymorphic"; "Inductive"; "Cumulativity"]; + optread = Flags.is_polymorphic_inductive_cumulativity; + optwrite = Flags.make_polymorphic_inductive_cumulativity } let _ = declare_int_option |