Evar_kinds
The kinds of existential variable
Should the obligation be defined (opaque or transparent (default)) or defined transparent and expanded in the term?
type question_mark = {
qm_obligation : obligation_definition_status; |
qm_name : Names.Name.t; |
qm_record_field : record_field option; |
}
val default_question_mark : question_mark
type t =
| ImplicitArg of Names.GlobRef.t * int * Names.Id.t option * bool | (* Force inference *) |
| BinderType of Names.Name.t | |
| EvarType of Names.Id.t option * Evar.t | |
| NamedHole of Names.Id.t | |
| QuestionMark of question_mark | |
| CasesType of bool | |
| InternalHole | |
| TomatchTypeParameter of Names.inductive * int | |
| GoalEvar | |
| ImpossibleCase | |
| MatchingVar of matching_var_kind | |
| VarInstance of Names.Id.t | |
| SubEvar of subevar_kind option * Evar.t |
type glob_evar_kind =
| GImplicitArg of Names.GlobRef.t * int * Names.Id.t option * bool | (* Force inference *) |
| GBinderType of Names.Name.t | |
| GNamedHole of bool * Names.Id.t | |
| GQuestionMark of question_mark | |
| GCasesType | |
| GInternalHole | |
| GImpossibleCase |