Module Firstorder_core_plugin.Sequent

type h_item = Names.GlobRef.t * Unify.Item.t option
type t
val has_fuel : t -> bool
val make_simple_atoms : t -> Formula.atoms
val iter_redexes : (Formula.any_formula -> unit) -> t -> unit
val deepen : t -> t
val record : Environ.env -> h_item -> t -> t
val lookup : Environ.env -> Evd.evar_map -> h_item -> t -> bool
val add_concl : flags:Formula.flags -> Environ.env -> Evd.evar_map -> EConstr.constr -> t -> t
val add_formula : flags:Formula.flags -> hint:bool -> Environ.env -> Evd.evar_map -> Names.GlobRef.t -> EConstr.constr -> t -> t
val re_add_formula_list : Evd.evar_map -> Formula.any_formula list -> t -> t
val find_left : Evd.evar_map -> Formula.atom -> t -> Names.GlobRef.t
val find_goal : Evd.evar_map -> t -> Names.GlobRef.t
val take_formula : Environ.env -> Evd.evar_map -> t -> Formula.any_formula * t
val empty_seq : int -> t
val extend_with_ref_list : flags:Formula.flags -> Environ.env -> Evd.evar_map -> Names.GlobRef.t list -> t -> t * Evd.evar_map
val extend_with_auto_hints : flags:Formula.flags -> Environ.env -> Evd.evar_map -> Hints.hint_db_name list -> t -> t * Evd.evar_map
val state : t -> Formula.Env.t