let backtrack (selection_lookahead: selection_lookahead) : unit =
selection_lookahead.sl_candidates#iter
(fun _ index ->
let remove_entries =
index#fold
(fun acc term raw_context_unifier ->
if Context_unifier.is_raw_context_unifier_invalid raw_context_unifier then
(term, raw_context_unifier) :: acc
else
acc
)
[]
in
List.iter
(fun (term, raw_context_unifier) ->
if not (index#remove term (Some raw_context_unifier)) then begin
print_endline (Term.term_to_string term);
print_endline (Context_unifier.raw_context_unifier_to_string raw_context_unifier);
failwith "Selection_lookahead.backtrack"
end;
selection_lookahead.sl_size <- selection_lookahead.sl_size - 1;
)
remove_entries
)