diff options
| author | coqbot-app[bot] | 2020-11-26 10:13:28 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-26 10:13:28 +0000 |
| commit | 02a04a2a98cc20c83f8465ab992e39ce4380f94e (patch) | |
| tree | 3313d2fc661f2c778a89679a04c981b78d5860a5 /engine/evar_kinds.ml | |
| parent | bef0e543b812764db985f64421265637501f5f8d (diff) | |
| parent | 47910007a9eff37c9f364a269b46874165711abf (diff) | |
Merge PR #13379: Add a new evar source to refer to evars which are types of evars
Reviewed-by: SkySkimmer
Diffstat (limited to 'engine/evar_kinds.ml')
| -rw-r--r-- | engine/evar_kinds.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml index 71d68f739e..fb41c4491e 100644 --- a/engine/evar_kinds.ml +++ b/engine/evar_kinds.ml @@ -40,6 +40,7 @@ type t = | ImplicitArg of GlobRef.t * (int * Id.t option) * bool (** Force inference *) | BinderType of Name.t + | EvarType of Id.t option * Evar.t (* type of an optionally named evar *) | NamedHole of Id.t (* coming from some ?[id] syntax *) | QuestionMark of question_mark | CasesType of bool (* true = a subterm of the type *) |