From 325258769b0a1a7059e77eb856590d2818722ada Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 26 Jul 2021 20:02:01 +0200
Subject: [PATCH] changelog

---
 CHANGELOG.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 897bc5fe1..fb5e992a0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -87,6 +87,9 @@ Coq 8.11 is no longer supported in this version of Iris.
   [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)
+* Rename the main entry point module for the proofmode from
+  `iris.proofmode.tactics` to `iris.proofmode.proofmode`. Under normal
+  circumstances, this should be the only proofmode file you need to import.
 
 **Changes in `bi`:**
 
@@ -152,6 +155,9 @@ s/\bbupd_forall\b/bupd_plain_forall/g
 # "global singleton" rename
 s/\b(inv|iris|(gen|inv)_heap|(Gen|Inv)Heap|proph_map|ProphMap|[oO]wnP|[hH]eap)G\b/\1GS/g
 s/\b([iI]nv|iris|(gen|inv)_heap|(Gen|Inv)Heap|proph_map|ProphMap|[oO]wnP|[hH]eap)PreG\b/\1GpreS/g
+# iris.proofmode.tactics → iris.proofmode.proofmode
+s/\bproofmode\.tactics\b/proofmode.proofmode/
+s/(From iris\.proofmode Require (Import|Export).*)\btactics\b/\1proofmode/
 EOF
 ```
 
-- 
GitLab