Merge pull request #48 from mdempsky/sepcancel-typo

Add missing parentheses in SepCancel's normalize2 tactic
This commit is contained in:
Adam Chlipala 2020-07-25 09:18:19 -04:00 committed by GitHub
commit e32105c142
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23

View file

@ -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.