add evars in sigma0 to roots in solution2evd

Author: Tragicus

src/coq_elpi_HOAS.ml

@@ -2570,10 +2570,16 @@ let reachable sigma roots acc =
       prlist_with_sep spc Evar.print (Evar.Set.elements res));
   res
 
+[%%if coq = "8.19"]
+let compute_roots sigma0 roots = Evd.fold_undefined (fun k _ acc -> Evar.Set.add k acc) sigma0 roots
+[%%else]
+let compute_roots sigma0 roots = Evar.Set.union (Evd.undefined_evars sigma0) (Evar.Set.union (Evd.defined_evars sigma0) roots)
+[%%endif]
+
 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