Commit 3875c726 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Give from_op_op a lower precedence so that it is not picked by default

when using iCombine.
parent 5b0f855e
...@@ -389,7 +389,7 @@ Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M ...@@ -389,7 +389,7 @@ Global Instance from_sep_big_sepL_app_persistent {A} (Φ : nat → A → uPred M
Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed. Proof. intros. by rewrite /FromAnd big_opL_app always_and_sep_l. Qed.
(* FromOp *) (* FromOp *)
Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a b) a b. Global Instance from_op_op {A : cmraT} (a b : A) : FromOp (a b) a b | 100.
Proof. by rewrite /FromOp. Qed. Proof. by rewrite /FromOp. Qed.
(* TODO: Worst case there could be a lot of backtracking on these instances, (* TODO: Worst case there could be a lot of backtracking on these instances,
......
Markdown is supported
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