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

Give the left instance of FromAnd (P1 ★ P2) P1 P2 precedence. 

That way type class search becomes more predictable.
parent 0f273374
Branches ci/maximedenes/instance-nobody-open-proof
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
proofmode/classes.v
+ 2
− 2
View file @ e423686f
...@@ -112,10 +112,10 @@ Global Arguments from_and : clear implicits. ...@@ -112,10 +112,10 @@ Global Arguments from_and : clear implicits.
Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2. Global Instance from_and_and P1 P2 : FromAnd (P1 ∧ P2) P1 P2.
Proof. done. Qed. Proof. done. Qed.
Global Instance from_and_sep_persistent_l P1 P2 : Global Instance from_and_sep_persistent_l P1 P2 :
PersistentP P1 → FromAnd (P1 ★ P2) P1 P2. PersistentP P1 → FromAnd (P1 ★ P2) P1 P2 | 9.
Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed. Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 : Global Instance from_and_sep_persistent_r P1 P2 :
PersistentP P2 → FromAnd (P1 ★ P2) P1 P2. PersistentP P2 → FromAnd (P1 ★ P2) P1 P2 | 10.
Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed. Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
Global Instance from_and_always P Q1 Q2 : Global Instance from_and_always P Q1 Q2 :
FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2). FromAnd P Q1 Q2 → FromAnd (□ P) (□ Q1) (□ Q2).
......
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