From 8eeef779da833c28e4955f71ec95077138dcb71f Mon Sep 17 00:00:00 2001
From: Daniel R. Grayson
Date: Tue, 27 Jan 2015 08:50:07 -0600
Subject: add -type-in-type to the usage message

---
 toplevel/usage.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index e9b5e8f84a..6909d89440 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -67,6 +67,7 @@ let print_usage_channel co command =
 \n  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)\
 \n  -impredicative-set     set sort Set impredicative\
 \n  -indices-matter        levels of indices (and nonuniform parameters) contribute to the level of inductives\
+\n  -type-in-type          disable universe consistency checking\
 \n  -time                  display the time taken by each command\
 \n  -no-native-compiler    disable the native_compute reduction machinery\
 \n  -h, -help              print this list of options\
-- 
cgit v1.2.3