Sequent (rocq-runtime.Firstorder_core

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.atoms -> 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 mem_hyp : Names.Id.t -> t -> bool

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