From ec7dd674ea25dfd36c007bb863fed63ce8d31ff2 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sat, 1 Sep 2018 12:39:09 -0700 Subject: Rewrite "Flags, Options and Tables" section. Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag: --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'doc/sphinx/proof-engine/ssreflect-proof-language.rst') diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 361b6e44a5..52609546d5 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -102,8 +102,8 @@ this corresponds to working in the following context: Unset Printing Implicit Defensive. .. seealso:: - :opt:`Implicit Arguments`, :opt:`Strict Implicit`, - :opt:`Printing Implicit Defensive` + :flag:`Implicit Arguments`, :flag:`Strict Implicit`, + :flag:`Printing Implicit Defensive` .. _compatibility_issues_ssr: @@ -2701,7 +2701,7 @@ typeclass inference. No inference for ``t``. Unresolved instances are quantified in the (inferred) type of ``t`` and abstracted in ``t``. -.. opt:: SsrHave NoTCResolution +.. flag:: SsrHave NoTCResolution This option restores the behavior of |SSR| 1.4 and below (never resolve typeclasses). @@ -3865,7 +3865,7 @@ duplication of function arguments. These copies usually end up in types hidden by the implicit arguments machinery or by user-defined notations. In these situations computing the right occurrence numbers is very tedious because they must be counted on the goal as printed -after setting the Printing All flag. Moreover the resulting script is +after setting the :flag:`Printing All` flag. Moreover the resulting script is not really informative for the reader, since it refers to occurrence numbers he cannot easily see. -- cgit v1.2.3