Commit 8d254aad authored by Dan Frumin's avatar Dan Frumin
Browse files

Coqify the comments.

parent bef526b4
...@@ -2,9 +2,9 @@ From iris.algebra Require Export frac auth updates local_updates. ...@@ -2,9 +2,9 @@ From iris.algebra Require Export frac auth updates local_updates.
From iris.algebra Require Import proofmode_classes. From iris.algebra Require Import proofmode_classes.
(** Authoritative CMRA where the NON-authoritative parts can be fractional. (** Authoritative CMRA where the NON-authoritative parts can be fractional.
This CMRA allows the original non-authoritative element `◯ a` to be split into This CMRA allows the original non-authoritative element [◯ a] to be split into
fractional parts `◯F{q} a`. Using `◯F a ≡ ◯F{1} a` is in effect the same as fractional parts [◯F{q} a]. Using [◯F a ≡ ◯F{1} a] is in effect the same as
using the original `◯ a`. Currently, however, this CMRA hides the ability to using the original [◯ a]. Currently, however, this CMRA hides the ability to
split the authoritative part into fractions. split the authoritative part into fractions.
*) *)
......
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