diff options
| author | Matthieu Sozeau | 2019-01-07 13:46:42 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-01-07 13:46:42 +0100 |
| commit | ffcb5526d33c1eaa2016dd3af9e3dffd932b7874 (patch) | |
| tree | 1e567b2f5dd90f9329a42ff2dcb0407277af5bd7 /vernac | |
| parent | 8c040974facb733682d24c488dc89941671f4ab7 (diff) | |
| parent | 0703cd1bbe5aab7e584d2293fe76c5f6ac4fe08c (diff) | |
Merge PR #8373: Fixes #8369: Not_found in printing message about an unresolved subevar.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/himsg.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index a2b5c8d70a..f3e1e1fc49 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -511,7 +511,7 @@ let pr_trailing_ne_context_of env sigma = if List.is_empty (Environ.rel_context env) && List.is_empty (Environ.named_context env) then str "." - else (str " in environment:"++ pr_context_unlimited env sigma) + else (strbrk " in environment:" ++ pr_context_unlimited env sigma) let rec explain_evar_kind env sigma evk ty = let open Evar_kinds in @@ -551,21 +551,21 @@ let rec explain_evar_kind env sigma evk ty = strbrk "an instance of type " ++ ty ++ str " for the variable " ++ Id.print id | Evar_kinds.SubEvar (where,evk') -> - let evi = Evd.find sigma evk' in + let rec find_source evk = + let evi = Evd.find sigma evk in + match snd evi.evar_source with + | Evar_kinds.SubEvar (_,evk) -> find_source evk + | src -> evi,src in + let evi,src = find_source evk' in let pc = match evi.evar_body with | Evar_defined c -> pr_leconstr_env env sigma c | Evar_empty -> assert false in let ty' = evi.evar_concl in - (match where with - | Some Evar_kinds.Body -> str "the body of " - | Some Evar_kinds.Domain -> str "the domain of " - | Some Evar_kinds.Codomain -> str "the codomain of " - | None -> - pr_existential_key sigma evk ++ str " of type " ++ ty ++ - str " in the partial instance " ++ pc ++ - str " found for ") ++ - explain_evar_kind env sigma evk' - (pr_leconstr_env env sigma ty') (snd evi.evar_source) + pr_existential_key sigma evk ++ + strbrk " in the partial instance " ++ pc ++ + strbrk " found for " ++ + explain_evar_kind env sigma evk + (pr_leconstr_env env sigma ty') src let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr sigma evi.evar_concl with |