Sequent (coq-core.Firstorder

type h_item = Names.GlobRef.t * (int * Constr.t) option

type history

type cmap

module HP : Heap.S with type elt = Formula.t

type t = private {

redexes : HP.t;

context : cmap;

latoms : Formula.atom list;

gl : EConstr.types;

glatom : Formula.atom option;

cnt : Formula.counter;

history : history;

depth : int;

}

val deepen : t -> t

val record : h_item -> t -> t

val lookup : Environ.env -> Evd.evar_map -> h_item -> t -> bool

val add_formula : flags:Formula.flags -> Environ.env -> Evd.evar_map -> Formula.side -> Names.GlobRef.t -> EConstr.constr -> t -> t

val re_add_formula_list : Evd.evar_map -> Formula.t list -> t -> t

val find_left : Evd.evar_map -> EConstr.constr -> t -> Names.GlobRef.t

val take_formula : Evd.evar_map -> t -> Formula.t * 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 print_cmap : cmap -> Pp.t