Universe Checking instead of Universes Checking

coq · Jun 4, 2019 · b870df1 · b870df1
1 parent 28838a4
commit b870df1
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1243,7 +1243,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
@@ -22,7 +22,7 @@ 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
@@ -1747,7 +1747,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) }