diff options
| author | Pierre-Marie Pédrot | 2018-03-27 13:34:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-03-27 13:34:14 +0200 |
| commit | 47ad058a918cb0fa8fef70fd7bd95bcb9ca05ee2 (patch) | |
| tree | e635d65f22b2b0f67b90ee6dd4ab8f339a4e5947 /engine/termops.ml | |
| parent | 01b7de3a673eb89cea61442c4db721aad9520c9f (diff) | |
| parent | 7fd28dc95e3251a10617ddb6758cc00b8960f954 (diff) | |
Merge PR #7062: Slightly refining some error messages about unresolvable evars.
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 3dfb0c34fd..b7531f6fc9 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -206,8 +206,12 @@ let 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 " ++ Id.print id - | Evar_kinds.SubEvar evk -> - str "subterm of " ++ Evar.print evk + | Evar_kinds.SubEvar (where,evk) -> + (match where with + | None -> str "subterm of " + | Some Evar_kinds.Body -> str "body of " + | Some Evar_kinds.Domain -> str "domain of " + | Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk let pr_evar_info evi = let open Evd in |