diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-07 12:47:08 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-07 15:18:48 +0100 |
| commit | fa906a5137058cf12444c70b76908b959012ce6d (patch) | |
| tree | 3d7075a34b8f11b17c810edb1fe2e109e67b178a /pretyping/evd.ml | |
| parent | 3af8f3e522bdf2bd103bb437c65ad79ae04ac9c3 (diff) | |
Improved tracking of the origin of evars.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 1d05d6c6e..c9435b54c 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1599,7 +1599,7 @@ let pr_decl ((id,b,_),ok) = | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ print_constr c ++ str (if ok then ")" else "}") -let pr_evar_source = function +let rec pr_evar_source = function | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType -> str "pattern-matching return predicate" | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id @@ -1615,6 +1615,7 @@ 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 " ++ pr_id id + | Evar_kinds.SubEvar k -> str "subterm of " ++ pr_evar_source k let pr_evar_info evi = let phyps = |