From b62320f274b221d44ef3fb9c17d1444cd1179ac6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 24 Jan 2019 14:51:16 +0100 Subject: [doc] more precise description of when automatic clears are triggered --- doc/sphinx/proof-engine/ssreflect-proof-language.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 8c1ca036cb..7c597d3ffa 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1601,7 +1601,7 @@ It interprets the top of the stack with the view :token:`term`. It is equivalent to :n:`move/@term`. A :token:`clear_switch` that immediately precedes an :token:`i_view` -is complemented with the name of the view whenever the :token:`i_view` +is complemented with the name of the view if an only if the :token:`i_view` is a simple proof context entry [#10]_. E.g. ``{}/v`` is equivalent to ``/v{v}``. This behavior can be avoided by separating the :token:`clear_switch` @@ -1636,8 +1636,8 @@ Intro patterns Note that defined constants cannot be introduced when δ-expansion is required to expose the top variable or assumption. A :token:`clear_switch` (even an empty one) immediately preceding an - :token:`ident` is complemented with that :token:`ident` if the identifier - is a simple proof context entry [#10]_. + :token:`ident` is complemented with that :token:`ident` if and only if + the identifier is a simple proof context entry [#10]_. As a consequence by prefixing the :token:`ident` with ``{}`` one can *replace* a context entry. This behavior can be avoided by separating the :token:`clear_switch` @@ -3077,7 +3077,7 @@ operation should be performed: A clear switch, even an empty one, is performed *after* the :token:`r_item` is actually processed and is complemented with the name of - the rewrite rule when it is a simple proof context entry [#10]_. + the rewrite rule if an only if it is a simple proof context entry [#10]_. As a consequence one can write ``rewrite {}H`` to rewrite with ``H`` and dispose ``H`` immediately afterwards. -- cgit v1.2.3