From e706afbf16c21fbc2ec21a3880330de3b5fefce9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 13 May 2022 09:49:29 +0200
Subject: [PATCH] fix some coqdoc warnings
---
iris/algebra/lib/ufrac_auth.v | 2 --
iris/proofmode/class_instances.v | 2 +-
2 files changed, 1 insertion(+), 3 deletions(-)
diff --git a/iris/algebra/lib/ufrac_auth.v b/iris/algebra/lib/ufrac_auth.v
index a31bdb83f..44966f828 100644
--- a/iris/algebra/lib/ufrac_auth.v
+++ b/iris/algebra/lib/ufrac_auth.v
@@ -9,9 +9,7 @@ difference:
if we have the authoritative element we can always increase its fraction
and allocate a new fragment.
- <<<
✓ (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.
[frac_auth_frag_validN_op_1_l]).
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 2e7b93e3d..32f3eb0ea 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
Import bi.
(* 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
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
--
GitLab