diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-09 12:09:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-11 18:34:04 +0100 |
| commit | 34cb1f6491017e4ed1a509f6b83b88a812ac425f (patch) | |
| tree | 0ad12f25af3050bb289147c54fe52f7349f2335e /intf/evar_kinds.mli | |
| parent | d083200ae5b391ceffaa0329a8e3a334036c7968 (diff) | |
Tentatively more informative report of failure when inferring
pattern-matching predicate.
Diffstat (limited to 'intf/evar_kinds.mli')
| -rw-r--r-- | intf/evar_kinds.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index f77fc5a6a..aae6e95aa 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -21,11 +21,11 @@ type t = * bool (** Force inference *) | BinderType of Name.t | QuestionMark of obligation_definition_status - | CasesType + | CasesType of bool (* true = a subterm of the type *) | InternalHole | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase | MatchingVar of bool * Id.t | VarInstance of Id.t - | SubEvar of t + | SubEvar of Constr.existential_key |