diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-01-22 15:05:08 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-01-22 15:05:08 +0100 |
| commit | d6bcc6ebe4f65d0555414851f7e4fb6fa1fb22a4 (patch) | |
| tree | d8617530b9cd67aafaf7674dcf2ed42c3265a433 /intf/evar_kinds.mli | |
| parent | f22969902223ab54f56f25583b24dc27c4cd6f4e (diff) | |
Adding a new evar source to remember the name of evars which were
named in the original term.
Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
Diffstat (limited to 'intf/evar_kinds.mli')
| -rw-r--r-- | intf/evar_kinds.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index afc5e3bab..470ad2a23 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -20,6 +20,7 @@ type t = | ImplicitArg of global_reference * (int * Id.t option) * bool (** Force inference *) | BinderType of Name.t + | NamedHole of Id.t (* coming from some ?[id] syntax *) | QuestionMark of obligation_definition_status | CasesType of bool (* true = a subterm of the type *) | InternalHole |