Skip to content
Snippets Groups Projects
Commit 095086fe authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix framing under conjunctions.

parent 7542306e
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
proofmode/class_instances.v
+ 1
− 1
View file @ 095086fe
...@@ -219,7 +219,7 @@ Global Instance make_and_true_l P : MakeAnd True P P. ...@@ -219,7 +219,7 @@ Global Instance make_and_true_l P : MakeAnd True P P.
Proof. by rewrite /MakeAnd left_id. Qed. Proof. by rewrite /MakeAnd left_id. Qed.
Global Instance make_and_true_r P : MakeAnd P True P. Global Instance make_and_true_r P : MakeAnd P True P.
Proof. by rewrite /MakeAnd right_id. Qed. Proof. by rewrite /MakeAnd right_id. Qed.
Global Instance make_and_default P Q : MakeSep P Q (P ★ Q) | 100. Global Instance make_and_default P Q : MakeAnd P Q (P ∧ Q) | 100.
Proof. done. Qed. Proof. done. Qed.
Global Instance frame_and_l R P1 P2 Q Q' : Global Instance frame_and_l R P1 P2 Q Q' :
Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9. Frame R P1 Q → MakeAnd Q P2 Q' → Frame R (P1 ∧ P2) Q' | 9.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment