package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

doc/firstorder_plugin/Firstorder_plugin/Sequent/index.html

Module Firstorder_plugin.SequentSource

Sourcetype h_item = Names.GlobRef.t * (int * Constr.t) option
Sourcetype history
Sourcetype cmap
module HP : Heap.S with type elt = Formula.t
Sourcetype t = private {
  1. redexes : HP.t;
  2. context : cmap;
  3. latoms : Formula.atom list;
  4. gl : EConstr.types;
  5. glatom : Formula.atom option;
  6. cnt : Formula.counter;
  7. history : history;
  8. depth : int;
}
Sourceval deepen : t -> t
Sourceval record : h_item -> t -> t
Sourceval lookup : Environ.env -> Evd.evar_map -> h_item -> t -> bool
Sourceval re_add_formula_list : Evd.evar_map -> Formula.t list -> t -> t
Sourceval take_formula : Evd.evar_map -> t -> Formula.t * t
Sourceval empty_seq : int -> t
Sourceval extend_with_ref_list : flags:Formula.flags -> Environ.env -> Evd.evar_map -> Names.GlobRef.t list -> t -> t * Evd.evar_map
Sourceval extend_with_auto_hints : flags:Formula.flags -> Environ.env -> Evd.evar_map -> Hints.hint_db_name list -> t -> t * Evd.evar_map
Sourceval print_cmap : cmap -> Pp.t