From 6907a08a35f5326ebb531a0ac4aa6a73daebaf07 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 3 Sep 2014 13:02:40 +0200
Subject: [PATCH] Make collection tactics work with guards.

---
 theories/collections.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/collections.v b/theories/collections.v
index 1313fc10..11294054 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -182,6 +182,7 @@ Ltac unfold_elem_of :=
     | context [ _ ∈ mret _ ] => setoid_rewrite elem_of_ret in H
     | context [ _ ∈ _ ≫= _ ] => setoid_rewrite elem_of_bind in H
     | context [ _ ∈ mjoin _ ] => setoid_rewrite elem_of_join in H
+    | context [ _ ∈ guard _; _ ] => setoid_rewrite elem_of_guard in H
     end);
   repeat match goal with
   | |- context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq
@@ -199,6 +200,7 @@ Ltac unfold_elem_of :=
   | |- context [ _ ∈ mret _ ] => setoid_rewrite elem_of_ret
   | |- context [ _ ∈ _ ≫= _ ] => setoid_rewrite elem_of_bind
   | |- context [ _ ∈ mjoin _ ] => setoid_rewrite elem_of_join
+  | |- context [ _ ∈ guard _; _ ] => setoid_rewrite elem_of_guard
   end.
 
 (** The tactic [solve_elem_of tac] composes the above tactic with [intuition].
-- 
GitLab