package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

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

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.15.0.tar.gz
sha256=73466e61f229b23b4daffdd964be72bd7a110963b9d84bd4a86bb05c5dc19ef3

doc/firstorder_plugin/Firstorder_plugin/Sequent/index.html

Module Firstorder_plugin.SequentSource

Sourcemodule CM : CSig.MapS with type key = Constr.t
Sourcetype h_item = Names.GlobRef.t * (int * Constr.t) option
Sourcemodule History : Stdlib.Set.S with type elt = h_item
Sourcemodule HP : Heap.S with type elt = Formula.t
Sourcetype t = {
  1. redexes : HP.t;
  2. context : Names.GlobRef.t list CM.t;
  3. latoms : EConstr.constr list;
  4. gl : EConstr.types;
  5. glatom : EConstr.constr option;
  6. cnt : Formula.counter;
  7. history : History.t;
  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 : Environ.env -> Evd.evar_map -> Names.GlobRef.t list -> t -> t * Evd.evar_map
Sourceval extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list -> t -> t * Evd.evar_map
Sourceval print_cmap : Names.GlobRef.t list CM.t -> Pp.t