Commit e706afbf authored by Ralf Jung's avatar Ralf Jung
Browse files

fix some coqdoc warnings

parent a1971471
Pipeline #65868 canceled with stage
in 4 minutes and 44 seconds
...@@ -9,9 +9,7 @@ difference: ...@@ -9,9 +9,7 @@ difference:
if we have the authoritative element we can always increase its fraction if we have the authoritative element we can always increase its fraction
and allocate a new fragment. and allocate a new fragment.
<<<
✓ (a ⋅ b) → ●U_p a ~~> ●U_(p + q) (a ⋅ b) ⋅ ◯U_q b ✓ (a ⋅ b) → ●U_p a ~~> ●U_(p + q) (a ⋅ b) ⋅ ◯U_q b
>>>
- We no longer have the [◯U{1} a] is the exclusive fragmental element (cf. - We no longer have the [◯U{1} a] is the exclusive fragmental element (cf.
[frac_auth_frag_validN_op_1_l]). [frac_auth_frag_validN_op_1_l]).
......
...@@ -6,7 +6,7 @@ From iris.prelude Require Import options. ...@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
Import bi. Import bi.
(* FIXME(Coq #6294): needs new unification *) (* FIXME(Coq #6294): needs new unification *)
(** The lemma [from_assumption_exact is not an instance, but defined using (** The lemma [from_assumption_exact] is not an instance, but defined using
[notypeclasses refine] through [Hint Extern] to enable the better unification [notypeclasses refine] through [Hint Extern] to enable the better unification
algorithm. We use [shelve] to avoid the creation of unshelved goals for evars algorithm. We use [shelve] to avoid the creation of unshelved goals for evars
by [refine], which otherwise causes TC search to fail. Such unshelved goals are by [refine], which otherwise causes TC search to fail. Such unshelved goals are
......
Supports Markdown
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