[ssr] compile "=> {} y" as "=> {y} y"

4 files changed, 25 insertions, 1 deletions

diff --git a/CHANGES.md b/CHANGES.md
index ae67eb5d1b..bcccd34774 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -160,6 +160,7 @@ SSReflect
   - block introduction: => [^ prefix ] [^~ suffix ]
   - fast introduction: => >
   - tactics as views: => /ltac:mytac
+  - replace hypothesis: => {}H
   See the reference manual for the actual documentation.
 
 Changes from 8.8.2 to 8.9+beta1
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 92bd4dbd1d..59d64feece 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1559,7 +1559,7 @@ whose general syntax is
    i_view ::= {? %{%} } /@term %| /ltac:( @tactic )
 
 .. prodn::
-   i_pattern ::= @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ]
+   i_pattern ::= {? %{%} } @ident %| > %| _ %| ? %| * %| + %| {? @occ_switch } -> %| {? @occ_switch }<- %| [ {?| @i_item } ] %| - %| [: {+ @ident } ]
 
 .. prodn::
    i_block ::= [^ @ident ] %| [^~ @ident ] %| [^~ @num ]
@@ -1615,6 +1615,10 @@ annotation: views are interpreted opening the ``ssripat`` scope.
   a new constant, fact, or defined constant :token:`ident`, respectively.
   Note that defined constants cannot be introduced when δ-expansion is
   required to expose the top variable or assumption.
+  An empty occurrence switch ``{}`` has the effect of clearing
+  the :token:`ident` before performing the introduction of :token:`ident`.
+  In other words by prefixing the :token:`ident` with ``{}`` one can
+  *replace* the context entry.
 ``>``
   pops every variable occurring in the rest of the stack.
   Type class instances are popped even if they don't occur
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 7f8825b89f..ce5fccec96 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -529,6 +529,8 @@ let tclCompileIPats l =
       (IOpView(Some [],v)) :: elab rest
   | (IPatClear cl) :: (IPatView v) :: rest ->
       (IOpView(None,v)) :: IOpClear cl :: elab rest
+  | (IPatClear []) :: (IPatId id) :: rest ->
+      (IOpClear [SsrHyp(None,id)]) :: IOpId id :: elab rest
 
   (* boring code *)
   | [] -> []
diff --git a/test-suite/ssr/ipat_replace.v b/test-suite/ssr/ipat_replace.v
new file mode 100644
index 0000000000..70e1d5bcf1
--- /dev/null
+++ b/test-suite/ssr/ipat_replace.v
@@ -0,0 +1,17 @@
+Require Import ssreflect.
+
+Lemma test : True.
+Proof.
+have H : True.
+  by [].
+have {}H : True.
+  by apply: H.
+by apply: H.
+Qed.
+
+Lemma test2 (H : True) : False -> False.
+Proof.
+Fail move=> {}W.
+move=> {}H.
+by apply: H.
+Qed.