diff --git a/CHANGES.md b/CHANGES.md
index d7a7eece9..415a31503 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -3,7 +3,7 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/),
 and this project adheres to [Semantic Versioning](https://semver.org/).
 
-## [Unreleased]
+## 2.5.0 (2024-02-25)
 
 ### Added
 
diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml
index 619fc678d..7083f0610 100644
--- a/src/handle/tactic.ml
+++ b/src/handle/tactic.ml
@@ -89,11 +89,13 @@ let tac_solve : popt -> proof_state -> proof_state = fun pos ps ->
     fatal pos "Unification goals are unsatisfiable.";
   (* compute the new list of goals by preserving the order of initial goals
      and adding the new goals at the end *)
-  let non_instantiated = function
-    | Typ gt -> !(gt.goal_meta.meta_value) = None
-    | _ -> assert false
+  let non_instantiated g =
+    match g with
+    | Typ gt when !(gt.goal_meta.meta_value) = None ->
+        Some (Goal.simpl Eval.simplify g)
+    | _ -> None
   in
-  let gs_typ = List.filter non_instantiated gs_typ in
+  let gs_typ = List.filter_map non_instantiated gs_typ in
   let is_eq_goal_meta m = function
     | Typ gt -> m == gt.goal_meta
     | _ -> assert false