diff options
| author |  Daniel R. Grayson <dan@math.uiuc.edu> | 2015-01-27 08:50:07 -0600 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-03-18 18:13:22 +0100 |
| commit | 8eeef779da833c28e4955f71ec95077138dcb71f (patch) | |
| tree | d62a501f3733f7be2e14e5cb072f4fe45c0e8158 /toplevel/usage.ml | |
| parent | 623a0e9bc07f19dacd8a25c33ebf1e68d9b3be30 (diff) | |
add -type-in-type to the usage message
Diffstat (limited to 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index e9b5e8f84..6909d8944 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\ |