summaryrefslogtreecommitdiff
path: root/pretyping/evd.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evd.ml')
-rw-r--r--pretyping/evd.ml10
1 files changed, 9 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5d6ca2ca..3cfad524 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -778,10 +778,18 @@ let pr_evar_info evi =
| Evar_empty -> mt ()
| Evar_defined c -> spc() ++ str"=> " ++ print_constr c
in
+ let candidates =
+ match evi.evar_body, evi.evar_candidates with
+ | Evar_empty, Some l ->
+ spc () ++ str "{" ++
+ prlist_with_sep (fun () -> str "|") print_constr l ++ str "}"
+ | _ ->
+ mt ()
+ in
let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in
hov 2
(str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]" ++
- spc() ++ src)
+ candidates ++ spc() ++ src)
let compute_evar_dependency_graph (sigma:evar_map) =
(* Compute the map binding ev to the evars whose body depends on ev *)