From 1d5431a48ab95efb2a98d1e1a1ca49183396b307 Mon Sep 17 00:00:00 2001
From: Maxime Buyse <maxime@cryspen.com>
Date: Wed, 1 Oct 2025 11:26:40 +0200
Subject: [PATCH] Switch hax-lib to edition 2021.

---
 CHANGELOG.md                    | 1 +
 hax-lib/Cargo.toml              | 2 +-
 hax-lib/macros/Cargo.toml       | 2 +-
 hax-lib/macros/types/Cargo.toml | 2 +-
 hax-lib/src/dummy.rs            | 2 +-
 5 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5028b9e82..775dd3f72 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -39,6 +39,7 @@ Change to cargo-hax:
 
 Changes to hax-lib:
 - New behavior for `hax_lib::include`: it now forces inclusion when in contradiction with `-i` flag.
+- hax-lib requires edition 2021 instead of 2024 (#1726)
 
 Changes to the Lean backend:
 - Improve support for functionalized loops (#1695)
diff --git a/hax-lib/Cargo.toml b/hax-lib/Cargo.toml
index 7ce6da77e..06e5b49e4 100644
--- a/hax-lib/Cargo.toml
+++ b/hax-lib/Cargo.toml
@@ -4,7 +4,7 @@ version.workspace = true
 authors.workspace = true
 license.workspace = true
 homepage.workspace = true
-edition.workspace = true
+edition = "2021"
 repository.workspace = true
 readme = "README.md"
 description = "Hax-specific helpers for Rust programs"
diff --git a/hax-lib/macros/Cargo.toml b/hax-lib/macros/Cargo.toml
index 885144866..b95c1c5e5 100644
--- a/hax-lib/macros/Cargo.toml
+++ b/hax-lib/macros/Cargo.toml
@@ -4,7 +4,7 @@ version.workspace = true
 authors.workspace = true
 license.workspace = true
 homepage.workspace = true
-edition.workspace = true
+edition = "2021"
 repository.workspace = true
 readme = "README.md"
 description = "Hax-specific proc-macros for Rust programs"
diff --git a/hax-lib/macros/types/Cargo.toml b/hax-lib/macros/types/Cargo.toml
index 8f08a14c1..574d6d22c 100644
--- a/hax-lib/macros/types/Cargo.toml
+++ b/hax-lib/macros/types/Cargo.toml
@@ -4,7 +4,7 @@ version.workspace = true
 authors.workspace = true
 license.workspace = true
 homepage.workspace = true
-edition.workspace = true
+edition = "2021"
 repository.workspace = true
 readme = "README.md"
 description = "Hax-internal types"
diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs
index 27f58241d..ca6283461 100644
--- a/hax-lib/src/dummy.rs
+++ b/hax-lib/src/dummy.rs
@@ -1,5 +1,5 @@
 mod abstraction;
-pub use abstraction::*;
+pub use abstraction::Concretization;
 
 pub mod prop;
 pub use prop::*;