pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Small patch for Coq 8.13

Browse source
This commit is contained in:
Adam Chlipala 2021-02-14 17:26:21 -05:00
parent f73e30817b
commit d1d44e55f6
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
ConcurrentSeparationLogic.v
View file

@ -698,7 +698,7 @@ Proof.
simp.
rewrite Heq in H0.
simp.
equality.
try equality.
cancel.
cancel.
cancel.
@ -823,7 +823,7 @@ Proof.
simp.
rewrite Heq in H0.
simp.
equality.
try equality.
cancel.
cancel.
cancel.

2
ConcurrentSeparationLogic_template.v
View file

@ -743,7 +743,7 @@ Proof.
simp.
rewrite Heq in H0.
simp.
equality.
try equality.
cancel.
cancel.
cancel.