From 63fa6d870d2bc2fb79ee65c0a5d63f899eaa7b0c Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Tue, 19 Mar 2024 11:09:17 +0100 Subject: [PATCH] add evars in sigma0 to roots in solution2evd --- src/coq_elpi_HOAS.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index d31e5071d..9101319de 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -2462,7 +2462,7 @@ let reachable sigma roots acc = let solution2evd sigma0 { API.Data.constraints; assignments; state; pp_ctx } roots = let state, solved_goals, _, _gls = elpi_solution_to_coq_solution ~calldepth:0 constraints state in let sigma = get_sigma state in - let roots = Evd.fold_undefined (fun k _ acc -> Evar.Set.add k acc) sigma0 roots in + let roots = Evar.Set.union (Evd.undefined_evars sigma0) (Evar.Set.union (Evd.defined_evars sigma0) roots) in let reachable_undefined_evars = reachable sigma roots Evar.Set.empty in let declared_goals, shelved_goals = get_declared_goals (Evar.Set.diff reachable_undefined_evars solved_goals) constraints state assignments pp_ctx in