diff options
| author | Gaëtan Gilbert | 2019-10-02 14:59:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-04 14:07:15 +0200 |
| commit | d7f43705e347f728d99e45720d8f2e0a3f7cff34 (patch) | |
| tree | 91c5ebaa86c5caab9171c2815dcdde5ea998f10a /toplevel/usage.ml | |
| parent | 87c17a6871ef4c21ff86a050297d33738c5a870a (diff) | |
Allow SProp default on
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 8555d78156..b17ca71f4c 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -79,6 +79,7 @@ let print_usage_common co command = \n -dump-glob f dump globalizations in file f (to be used by coqdoc)\ \n -impredicative-set set sort Set impredicative\ \n -allow-sprop allow using the proof irrelevant SProp sort\ +\n -disallow-sprop forbid using the proof irrelevant SProp sort\ \n -sprop-cumulative make sort SProp cumulative with the rest of the hierarchy\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ |