mlRewriteBy ... in ... suceeds, even if LHS doesn't appear in the hypothesis, but it appears in the goal.

[Thrithralas]

Take the following example:

Example wrong
    {Σ : Signature}
    {syntax : Syntax}
    (Γ : Theory)
    (a b : Pattern) :
    theory ⊆ Γ ->
    well_formed a = true ->
    well_formed b = true ->
    Γ ⊢ a =ml b ---> b ---> a.
Proof.
  intros.
  mlIntro. mlIntro.
  mlRewriteBy "0" at 1 in "1".
Abort.

"1" has no occurences of the pattern a in it, yet mlRewriteBy "0" at 1 in "1". still suceeds by rewriting the goal to b. This is due to mlRewriteBy ... in ... reverting the hypothesis, then applying the standard mlRewriteBy tactic, in which case the goal has an occurence, even if the hypothesis did not.

This was a known bug in #441, but the solution to this does not seem obvious.