package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type obligation_definition_status =
  1. | Define of bool
  2. | Expand
type matching_var_kind =
  1. | FirstOrderPatVar of Names.Id.t
  2. | SecondOrderPatVar of Names.Id.t
type subevar_kind =
  1. | Domain
  2. | Codomain
  3. | Body
type record_field = {
  1. fieldname : Names.Constant.t;
  2. recordname : Names.inductive;
}
type question_mark = {
  1. qm_obligation : obligation_definition_status;
  2. qm_name : Names.Name.t;
  3. qm_record_field : record_field option;
}
val default_question_mark : question_mark
type t =
  1. | ImplicitArg of Names.GlobRef.t * int * Names.Id.t option * bool
  2. | BinderType of Names.Name.t
  3. | NamedHole of Names.Id.t
  4. | QuestionMark of question_mark
  5. | CasesType of bool
  6. | InternalHole
  7. | TomatchTypeParameter of Names.inductive * int
  8. | GoalEvar
  9. | ImpossibleCase
  10. | MatchingVar of matching_var_kind
  11. | VarInstance of Names.Id.t
  12. | SubEvar of subevar_kind option * Evar.t