fix: disable memoize in pattern conv

src/Init/Conv.lean

@@ -33,7 +33,7 @@ occurrence of the pattern.
 syntax occsIndexed := num+
 
 /-- An occurrence specification, either `*` or a list of numbers. The default is `[1]`. -/
-syntax occs := atomic(" (" &"occs") " := " (occsWildcard <|> occsIndexed) ")"
+syntax occs := atomic("(" &"occs") " := " (occsWildcard <|> occsIndexed) ") "
 
 /--
 `with_annotate_state stx t` annotates the lexical range of `stx : Syntax` with

src/Lean/Elab/Tactic/Conv/Pattern.lean

@@ -125,7 +125,8 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
         pure (.occs #[] 0 ids.toList)
       | _ => throwUnsupportedSyntax
     let state ← IO.mkRef occs
-    let (result, _) ← Simp.main lhs (← getContext) (methods := { pre := pre patternA state })
+    let ctx := { ← getContext with config.memoize := occs matches .all _ }
+    let (result, _) ← Simp.main lhs ctx (methods := { pre := pre patternA state })
     let subgoals ← match ← state.get with
     | .all #[] | .occs _ 0 _ =>
       throwError "'pattern' conv tactic failed, pattern was not found{indentExpr patternA.expr}"

tests/lean/conv1.lean

@@ -245,3 +245,7 @@ example : ((x + y) + z : Nat) = x + (y + z) := by conv => pattern (occs := 1 2 5
 
 macro "bla" : term => `(?a)
 example : 1 = 1 := by conv => apply bla; congr
+
+example (h : a = a') (H : a + a' = 0) : a + a = 0 := by
+  conv in (occs := 2) a => rw [h]
+  apply H