From 410d5aa6dd45055ed05fe094860dd00cbc772030 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl> Date: Sun, 25 Jul 2021 22:28:07 +0000 Subject: [PATCH] More precise link --- CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3843ddcd6..38dd45048 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -78,7 +78,8 @@ Coq 8.11 is no longer supported in this version of Iris. To adjust your code if you use such logics and define `Frame` instances, ensure these instances to have priority at least 2: they should have either at least 2 (non-dependent) premises, or an explicit priority. - References: docs for `frame_here_absorbing` and + References: docs for `frame_here_absorbing` in + [iris/proofmode/frame_instances.v](iris/proofmode/frame_instances.v) and https://coq.inria.fr/refman/addendum/type-classes.html#coq:cmd.Instance. (by Paolo G. Giarrusso, BedRock Systems) -- GitLab