Commit 83b31bbd authored by Robbert Krebbers's avatar Robbert Krebbers

Make ambigious argument explicit.

To prepare for https://github.com/coq/coq/pull/10762
parent 84d73de1
...@@ -622,7 +622,7 @@ Qed. ...@@ -622,7 +622,7 @@ Qed.
Global Instance id_free_op_r x y : IdFree y Cancelable x IdFree (x y). Global Instance id_free_op_r x y : IdFree y Cancelable x IdFree (x y).
Proof. Proof.
intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?. intros ?? z ? Hid%symmetry. revert Hid. rewrite -assoc=>/(cancelableN x) ?.
eapply (id_free0_r _); [by eapply cmra_validN_op_r |symmetry; eauto]. eapply (id_free0_r y); [by eapply cmra_validN_op_r |symmetry; eauto].
Qed. Qed.
Global Instance id_free_op_l x y : IdFree x Cancelable y IdFree (x y). Global Instance id_free_op_l x y : IdFree x Cancelable y IdFree (x y).
Proof. intros. rewrite comm. apply _. Qed. Proof. intros. rewrite comm. apply _. Qed.
......
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