Commit 69dfcc71 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Merge branch 'master' into 'master'

Fix notation in comments

See merge request !447
parents fdda97e8 8d254aad
Pipeline #28587 passed with stage
in 20 minutes and 41 seconds
......@@ -2,9 +2,9 @@ From iris.algebra Require Export frac auth updates local_updates.
From iris.algebra Require Import proofmode_classes.
(** Authoritative CMRA where the NON-authoritative parts can be fractional.
This CMRA allows the original non-authoritative element `◯ a` to be split into
fractional parts `◯!{q} a`. Using `◯! a ≡ ◯!{1} a` is in effect the same as
using the original `◯ a`. Currently, however, this CMRA hides the ability to
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
using the original [◯ a]. Currently, however, this CMRA hides the ability to
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