Added a printing function to handle single evars

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14682 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 404e1b6ae7..8727f10228 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -294,6 +294,12 @@ let pr_evgl_sign gl =
   let pc = pr_lconstr gl.evar_concl in
   hov 0 (str"[" ++ ps ++ spc () ++ str"|- "  ++ pc ++ str"]" ++ spc () ++ warn)
 
+(* Print an existential variable *)
+
+let pr_evar (ev, evd) =
+  let pegl = pr_evgl_sign evd in
+  (hov 0 (str (string_of_existential ev)  ++ str " : " ++ pegl))
+
 (* Print an enumerated list of existential variables *)
 let rec pr_evars_int i = function
   | [] -> (mt ())