non-looping rwHyps

coq-community · Jan 10, 2024 · 5713ab9 · 5713ab9
1 parent 6da5cc8
commit 5713ab9
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/theories/Tactics/Forward.v b/theories/Tactics/Forward.v
@@ -19,8 +19,11 @@ Ltac forward_reason :=
 
 Ltac rwHyps :=
   repeat match goal with
-           [ H: _ = _ |- _] =>  rewrite -> H
-         end.
+           [ H: ?l = ?r |- _] =>
+           match r with
+           | context [l] => idtac
+           | _ => rewrite -> H
+           end
 
 Ltac rwHypsR :=
   repeat match goal with