Commit 9e4c13a3 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

More coherent name for positiveR.

parent 6ca015ff
...@@ -960,9 +960,9 @@ Section positive. ...@@ -960,9 +960,9 @@ Section positive.
- intros ???. apply Pos.add_assoc. - intros ???. apply Pos.add_assoc.
- intros ??. apply Pos.add_comm. - intros ??. apply Pos.add_comm.
Qed. Qed.
Canonical Structure posR : cmraT := discreteR positive pos_ra_mixin. Canonical Structure positiveR : cmraT := discreteR positive pos_ra_mixin.
Global Instance pos_cmra_discrete : CMRADiscrete posR. Global Instance pos_cmra_discrete : CMRADiscrete positiveR.
Proof. constructor; apply _ || done. Qed. Proof. constructor; apply _ || done. Qed.
End positive. End positive.
......
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