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