From c9d7a692879df71aa57cbf86131d02e87e1364ae Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@csail.mit.edu>
Date: Tue, 19 Apr 2016 19:16:14 -0400
Subject: [PATCH] SepCancel: now less conservative

---
 SepCancel.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/SepCancel.v b/SepCancel.v
index a2392c7..eceb95d 100644
--- a/SepCancel.v
+++ b/SepCancel.v
@@ -277,7 +277,7 @@ Module Make(Import S : SEP).
 
   Ltac forAllAtoms p k :=
     match p with
-      | ?q * ?r => (forAllAtoms q k || forAllAtoms r k) || fail 2
+      | ?q * ?r => forAllAtoms q k || forAllAtoms r k
       | _ => k p
     end.