diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml
index fa89fbcaa..b55e9bf2c 100644
--- a/src/ecHiGoal.ml
+++ b/src/ecHiGoal.ml
@@ -796,9 +796,10 @@ let process_rewrite1_core
           tc_error !!tc "context variable does not appear in the r-pattern"
 
 (* -------------------------------------------------------------------- *)
-let process_delta ?target ((s :rwside), o, p) tc =
+let process_delta ?(rigid = false) ?target ((s :rwside), o, p) tc =
   let env, hyps, concl = FApi.tc1_eflat tc in
   let o = norm_rwocc o in
+  let occmode = if rigid then Some om_rigid else None in
 
   let idtg, target =
     match target with
@@ -865,7 +866,7 @@ let process_delta ?target ((s :rwside), o, p) tc =
   match s with
   | `LtoR -> begin
     let matches =
-      try  ignore (PT.pf_find_occurence ptenv ~ptn:p target); true
+      try  ignore (PT.pf_find_occurence ptenv ?occmode ~ptn:p target); true
       with PT.FindOccFailure _ -> false
     in
 
@@ -926,23 +927,26 @@ let process_delta ?target ((s :rwside), o, p) tc =
         with EcEnv.NotReducible -> fp
     in
 
-    let matches =
-      try  ignore (PT.pf_find_occurence ptenv ~ptn:fp target); true
-      with PT.FindOccFailure _ -> false
-    in
+    begin
+      match PT.pf_find_occurence ?occmode ptenv ~ptn:fp target with
+      | (_, occmode) ->
+        let p    = concretize_form ptenv p  in
+        let fp   = concretize_form ptenv fp in
+        let cpos =
+          try
+            FPosition.select_form
+              ?xconv:(if rigid then Some `AlphaEq else None)
+              ?keyed:(if rigid then Some occmode.k_keyed else None)
+              hyps o fp target
+          with InvalidOccurence ->
+            tc_error !!tc "invalid occurences selector" in
 
-    if matches then begin
-      let p    = concretize_form ptenv p  in
-      let fp   = concretize_form ptenv fp in
-      let cpos =
-        try  FPosition.select_form hyps o fp target
-        with InvalidOccurence ->
-          tc_error !!tc "invalid occurences selector"
-      in
+        let target = FPosition.map cpos (fun _ -> p) target in
+        t_change ~ri ?target:idtg target tc 
 
-      let target = FPosition.map cpos (fun _ -> p) target in
-      t_change ~ri ?target:idtg target tc
-    end else t_id tc
+      | exception (PT.FindOccFailure _) ->
+        t_id tc
+  end
 
 (* -------------------------------------------------------------------- *)
 let process_rewrite1_r ttenv ?target ri tc =
@@ -964,12 +968,12 @@ let process_rewrite1_r ttenv ?target ri tc =
       let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in
       t_simplify_lg ?target ~delta:`IfApplied (ttenv, logic) tc
 
-  | RWDelta (rwopt, p) -> begin
+  | RWDelta (rigid, rwopt, p) -> begin
       if Option.is_some rwopt.match_ then
         tc_error !!tc "cannot use pattern selection in delta-rewrite rules";
 
       let do1 tc =
-        process_delta ?target (rwopt.side, rwopt.occurrence, p) tc in
+        process_delta ~rigid ?target (rwopt.side, rwopt.occurrence, p) tc in
 
       match rwopt.repeat with
       | None -> do1 tc
diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli
index c970cbe63..a283665ed 100644
--- a/src/ecHiGoal.mli
+++ b/src/ecHiGoal.mli
@@ -79,7 +79,7 @@ val process_clear       : clear_info -> backward
 val process_smt         : ?loc:EcLocation.t -> ttenv -> pprover_infos option -> backward
 val process_coq         : loc:EcLocation.t -> name:string -> ttenv -> EcProvers.coq_mode option -> pprover_infos -> backward
 val process_apply       : implicits:bool -> apply_t * prevert option -> backward
-val process_delta       : ?target:psymbol -> (rwside * rwocc * pformula) -> backward
+val process_delta       : ?rigid:bool -> ?target:psymbol -> (rwside * rwocc * pformula) -> backward
 val process_rewrite     : ttenv -> ?target:psymbol -> rwarg list -> backward
 val process_subst       : pformula list -> backward
 val process_cut         : ?mode:cutmode -> engine -> ttenv -> cut_t -> backward
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 8d05c2a2b..9552a74a1 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -2450,8 +2450,8 @@ rwarg1:
 | side=rwside repeat=rwrepeat? occurrence=rwocc? match_=bracket(rwmatch)? fp=rwpterms
    { RWRw ({ side; repeat; occurrence; match_ }, fp) }
 
-| side=rwside repeat=rwrepeat? occurrence=rwocc? SLASH fp=sform_h %prec prec_tactic
-   { RWDelta ({ side; repeat; occurrence; match_ = None }, fp); }
+| side=rwside repeat=rwrepeat? occurrence=rwocc? SLASH rigid=iboption(TILD) fp=sform_h %prec prec_tactic
+   { RWDelta (rigid, { side; repeat; occurrence; match_ = None }, fp); }
 
 | PR s=bracket(rwpr_arg)
    { RWPr s }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 71ad8c642..2a70a2e92 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -1001,7 +1001,7 @@ type rwarg = (tfocus located) option * rwarg1 located
 
 and rwarg1 =
   | RWSimpl  of [`Default | `Variant]
-  | RWDelta  of (rwoptions * pformula)
+  | RWDelta  of (bool * rwoptions * pformula)
   | RWRw     of (rwoptions * (rwside * ppterm) list)
   | RWPr     of (psymbol * pformula option)
   | RWDone   of [`Default | `Variant] option