Adam Chlipala
|
f3211734b9
|
A big pass to stop Coq from complaining about missing locality annotations
|
2022-03-07 13:48:40 -05:00 |
|
Matthew Dempsky
|
0a55c03aa0
|
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
|
2020-07-24 18:23:44 -07:00 |
|
Adam Chlipala
|
daac5734b0
|
Finalizing ConcurrentSeparationLogic
|
2016-05-01 19:45:51 -04:00 |
|
Adam Chlipala
|
035bfa57ee
|
Make SepCancel more conservative
|
2016-05-01 18:53:25 -04:00 |
|
Adam Chlipala
|
a242a93a7e
|
ConcurrentSeparationLogic: a producer-consumer example (after tweaking SepCancel)
|
2016-04-28 10:03:10 -04:00 |
|
Adam Chlipala
|
47fd9a8abf
|
SepCancel: adapt for Coq versions
|
2016-04-20 08:36:48 -04:00 |
|
Adam Chlipala
|
4209399eb1
|
Comment SeparationLogic, while getting it working with Coq 8.4
|
2016-04-19 21:25:39 -04:00 |
|
Adam Chlipala
|
c9d7a69287
|
SepCancel: now less conservative
|
2016-04-19 19:16:14 -04:00 |
|
Adam Chlipala
|
60c21c07ec
|
SepCancel: be more cautious in a few ways
|
2016-04-19 18:36:25 -04:00 |
|
Adam Chlipala
|
e1844abf25
|
Factor out SepCancel
|
2016-04-19 14:28:30 -04:00 |
|