diff options
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 2 | ||||
| -rw-r--r-- | test-suite/success/typing_flags.v | 4 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 8d7bf78a85..c391cc949d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1224,7 +1224,7 @@ Controlling Typing Flags break the consistency of the system, use at your own risk. Unchecked (co)inductive types are printed by :cmd:`Print Assumptions`. -.. flag:: Universes Checking +.. flag:: Universe Checking This option can be used to enable/disable the checking of universes, providing a form of "type in type". Warning: this breaks the consistency of the system, use diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v index 31550b45a6..c15701e000 100644 --- a/test-suite/success/typing_flags.v +++ b/test-suite/success/typing_flags.v @@ -16,13 +16,13 @@ Set Guard Checking. Print Assumptions f. -Unset Universes Checking. +Unset Universe Checking. Definition T := Type. Fixpoint g (n : nat) : T := T. Print Typing Flags. -Set Universes Checking. +Set Universe Checking. Fail Definition g2 (n : nat) : T := T. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f90439d222..8712b8e958 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1744,7 +1744,7 @@ let _ = declare_bool_option { optdepr = false; optname = "universes checking"; - optkey = ["Universes"; "Checking"]; + optkey = ["Universe"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_universes); optwrite = (fun b -> Global.set_check_universes b) } |