Sequent (coq-core.Firstorder

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 : 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 -> EConstr.constr -> t -> Names.GlobRef.t

val find_goal : Evd.evar_map -> t -> Names.GlobRef.t

val take_formula : 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