diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index cd23e6849fb45207441909ce86447db258507c75..fcfb38bee6cd80e33ece13dc6a48919fbf0e7aab 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -530,7 +530,7 @@ Tactic Notation "wp_store" :=
   | _ => fail "wp_store: not a 'wp'"
   end.
 
-Local Ltac solve_vals_cas_compare_safe :=
+Ltac solve_vals_cas_compare_safe :=
   (* The first branch is for when we have [vals_cas_compare_safe] in the context.
      The other two branches are for when either one of the branches reduces to
      [True] or we have it in the context. *)