Commit 9f19f1ab authored by Robbert Krebbers's avatar Robbert Krebbers

Fix typo.

parent 232a2e93
......@@ -887,7 +887,7 @@ End discrete_ofe.
Notation discreteO A := (OfeT A (discrete_ofe_mixin _)).
(** Force the [Equivalence] proof to be [eq_equivalence] so that it does not
find another one, like [ofe_equivalence], in the case of aliases. See also *) *)
Notation leibnizO A := (OfeT A (@discrete_ofe_mixin _ equivL eq_equivalence)).
(** In order to define a discrete CMRA with carrier [A] (in the file [cmra.v])
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