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.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c

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
Sourcetype glob_evar_kind =
  1. | GImplicitArg of Names.GlobRef.t * int * Names.Id.t option * bool
    (*

    Force inference

    *)
  2. | GBinderType of Names.Name.t
  3. | GNamedHole of bool * Names.Id.t
  4. | GQuestionMark of question_mark
  5. | GCasesType
  6. | GInternalHole
  7. | GImpossibleCase