From 73475b844cb09f06c78d8f8a426e9de0eeffc367 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 18 Oct 2019 14:43:11 +0100
Subject: Coq: tweak a state monad lifting rule to improve performance

---
 lib/coq/Sail2_state_lemmas.v | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_state_lemmas.v b/lib/coq/Sail2_state_lemmas.v
index 49d35770..90ae6840 100644
--- a/lib/coq/Sail2_state_lemmas.v
+++ b/lib/coq/Sail2_state_lemmas.v
@@ -306,8 +306,15 @@ destruct c; reflexivity.
 Qed.
 Hint Resolve liftState_if_distrib_sumbool : liftState.
 (* As above, but simple apply doesn't seem to work (again, due to unification problems
-   with the M alias for monad *)
-Hint Extern 0 (liftState _ _ = _) => apply liftState_if_distrib_sumbool : liftState.
+   with the M alias for monad).  Be careful about only applying to a suitable goal to
+   avoid slowing down proofs. *)
+Hint Extern 0 (liftState _ ?t = _) =>
+  match t with
+  | match ?x with _ => _ end =>
+    match type of x with
+    | sumbool _ _ => apply liftState_if_distrib_sumbool
+    end
+  end : liftState.
 
 Lemma liftState_let_pair Regs RegVal A B C E r (x : B * C) M :
   @liftState Regs RegVal A E r (let '(y, z) := x in M y z) =
-- 
cgit v1.2.3