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/coq-core.engine/Evar_kinds/index.html

Module Evar_kindsSource

The kinds of existential variable

Should the obligation be defined (opaque or transparent (default)) or defined transparent and expanded in the term?

Sourcetype obligation_definition_status =
  1. | Define of bool
  2. | Expand
Sourcetype matching_var_kind =
  1. | FirstOrderPatVar of Names.Id.t
  2. | SecondOrderPatVar of Names.Id.t
Sourcetype subevar_kind =
  1. | Domain
  2. | Codomain
  3. | Body
Sourcetype record_field = {
  1. fieldname : Names.Constant.t;
  2. recordname : Names.inductive;
}
Sourcetype question_mark = {
  1. qm_obligation : obligation_definition_status;
  2. qm_name : Names.Name.t;
  3. qm_record_field : record_field option;
}
Sourceval default_question_mark : question_mark
Sourcetype t =
  1. | ImplicitArg of Names.GlobRef.t * int * Names.Id.t option * bool
    (*

    Force inference

    *)
  2. | BinderType of Names.Name.t
  3. | EvarType of Names.Id.t option * Evar.t
  4. | NamedHole of Names.Id.t
  5. | QuestionMark of question_mark
  6. | CasesType of bool
  7. | InternalHole
  8. | TomatchTypeParameter of Names.inductive * int
  9. | GoalEvar
  10. | ImpossibleCase
  11. | MatchingVar of matching_var_kind
  12. | VarInstance of Names.Id.t
  13. | SubEvar of subevar_kind option * Evar.t