diff options
| author | Pierre-Marie Pédrot | 2020-04-23 14:53:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-23 14:53:23 +0200 |
| commit | 48f73e492465f3c46438583c069bc0ba745ef56f (patch) | |
| tree | e499cc660630fcadd08aff5a127a8c34455d664d /doc/sphinx | |
| parent | 7863c12930687e1e2dc982d9b406fb4d6e7a02c1 (diff) | |
| parent | 3231196c77c0641d7c59191bf691378b334afc46 (diff) | |
Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/sprop.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 2 |
2 files changed, 9 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. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a0d1080314..60fdbf0a9d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1096,6 +1096,8 @@ Controlling Typing Flags Print the status of the three typing flags: guard checking, positivity checking and universe checking. +See also :flag:`Cumulative StrictProp` in the |SProp| chapter. + .. example:: .. coqtop:: all reset |