summaryrefslogtreecommitdiff
path: root/pretyping/evd.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
commit86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree9b221c283c2971f7ac151397231059e1d239e723 /pretyping/evd.ml
parent39efc41237ec906226a3a53d7396d51173495204 (diff)
parent61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)
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 *)