From 72595700c23868169edd1296bab283bb5e40d20c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 19 Jun 2019 00:00:10 +0200
Subject: [PATCH] export solve_vals_cas_compare_safe
---
theories/heap_lang/proofmode.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index cd23e6849..fcfb38bee 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. *)
--
GitLab