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 /pretyping/evd.ml | |
| parent | d083200ae5b391ceffaa0329a8e3a334036c7968 (diff) | |
Tentatively more informative report of failure when inferring
pattern-matching predicate.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index c9435b54c..0fe16f0ed 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1601,7 +1601,9 @@ let pr_decl ((id,b,_),ok) = let rec pr_evar_source = function | Evar_kinds.QuestionMark _ -> str "underscore" - | Evar_kinds.CasesType -> str "pattern-matching return predicate" + | Evar_kinds.CasesType false -> str "pattern-matching return predicate" + | Evar_kinds.CasesType true -> + str "subterm of pattern-matching return predicate" | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder" | Evar_kinds.ImplicitArg (c,(n,ido),b) -> @@ -1615,7 +1617,8 @@ let rec pr_evar_source = function | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause" | Evar_kinds.MatchingVar _ -> str "matching variable" | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id - | Evar_kinds.SubEvar k -> str "subterm of " ++ pr_evar_source k + | Evar_kinds.SubEvar evk -> + str "subterm of " ++ str (string_of_existential evk) let pr_evar_info evi = let phyps = |