pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-27 23:06:20 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Add missing parentheses in SepCancel's normalize2 tactic

Browse source 
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
This commit is contained in:
Matthew Dempsky 2020-07-24 18:23:44 -07:00
parent d1ace360eb
commit 0a55c03aa0
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
SepCancel.v
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.