search

achlipala / frap

Formal Reasoning About Programs
Other
657 stars 82 forks source link

Add missing parentheses in SepCancel's normalize2 tactic #48

Closed mdempsky closed 4 years ago

mdempsky commented 4 years ago

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