Simplify added goals + prepare new release (#1056)

* simplify added goals (fix a change in #1052 for lambdapi-stdlib to compile)
* prepare release

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
 

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