diff --git a/SepCancel.v b/SepCancel.v index 9b5b8df..71b46ff 100644 --- a/SepCancel.v +++ b/SepCancel.v @@ -252,7 +252,7 @@ Module Make(Import S : SEP). Ltac normalize2 := match goal with - | [ |- context[star ?p lift (?P /\ ?Q)] ] => rewrite (lift_uncombine p P Q) + | [ |- context[star ?p (lift (?P /\ ?Q))] ] => rewrite (lift_uncombine p P Q) | [ |- context[star ?p (star ?q ?r)] ] => rewrite (star_assoc p q r) end.