From 24701948804ecdc7c2518773fd66308913441195 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 3 Jun 2019 17:17:35 +0200
Subject: Universe Checking instead of Universes Checking

---
 doc/sphinx/proof-engine/vernacular-commands.rst | 2 +-
 test-suite/success/typing_flags.v               | 4 ++--
 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) }
 
-- 
cgit v1.2.3