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

Make ambigious argument explicit. 

To prepare for https://github.com/coq/coq/pull/10762
parent fad7bbcf
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/algebra/cmra.v
+ 1
− 1
View file @ d9662274
...@@ -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.
......
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