diff options
| author | Gaëtan Gilbert | 2020-04-06 14:41:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-16 23:10:03 +0200 |
| commit | 3231196c77c0641d7c59191bf691378b334afc46 (patch) | |
| tree | aa10bcb9d93072e4808e831d4e4a73f88ad47349 /doc/sphinx/addendum | |
| parent | 988e195c2cd0d97b664193bf1c83c3da2b380f7c (diff) | |
Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 9acdd18b89..b2d3687780 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -240,3 +240,10 @@ so correctly converts ``x`` and ``y``. the kernel when it is passed a term with incorrect relevance marks. To avoid conversion issues as in ``late_mark`` you may wish to use it to find when your tactics are producing incorrect marks. + +.. flag:: Cumulative StrictProp + :name: Cumulative StrictProp + + Set this flag (it is off by default) to make the kernel accept + cumulativity between |SProp| and other universes. This makes + typechecking incomplete. |