From 0a55c03aa08b5932ebdbe6089c2ab892c6d8e762 Mon Sep 17 00:00:00 2001
From: Matthew Dempsky <matthew@dempsky.org>
Date: Fri, 24 Jul 2020 18:23:44 -0700
Subject: [PATCH] Add missing parentheses in SepCancel's normalize2 tactic

Before this change, "Print normalize2" prints:

    Ltac Frap.SepCancel.Make.normalize2 :=
      match goal with
      | |- context [ (?p * lift) (?P /\ ?Q) ] => rewrite (lift_uncombine p P Q)
      | |- context [ ?p * (?q * ?r) ] => rewrite (star_assoc p q r)
      end

After, it prints:

    Ltac Frap.SepCancel.Make.normalize2 :=
      match goal with
      | |- context [ ?p * [|?P /\ ?Q|] ] => rewrite (lift_uncombine p P Q)
      | |- context [ ?p * (?q * ?r) ] => rewrite (star_assoc p q r)
      end
---
 SepCancel.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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.