sig
type literal = Term.literal
type raw_context_unifier = Context_unifier.raw_context_unifier
type selection_lookahead
val create : int -> Selection_lookahead.selection_lookahead
val is_full : Selection_lookahead.selection_lookahead -> bool
val add :
no_duplicates:bool ->
Selection_lookahead.selection_lookahead ->
Selection_lookahead.literal ->
Selection_lookahead.raw_context_unifier -> unit
val check :
Selection_lookahead.selection_lookahead ->
Selection_lookahead.literal -> bool
val backtrack : Selection_lookahead.selection_lookahead -> unit
end