diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 02e836819..a6c55013a 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -2570,10 +2570,13 @@ let reachable sigma roots acc = prlist_with_sep spc Evar.print (Evar.Set.elements res)); res +let compute_roots sigma0 roots = + Evd.fold (fun k _ acc -> Evar.Set.add k acc) sigma0 roots + let solution2evd ~eta_contract_solution sigma0 { API.Data.constraints; assignments; state; pp_ctx } roots = let state, solved_goals, _, _gls = elpi_solution_to_coq_solution ~eta_contract_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 = compute_roots 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