Merge PR#722: [printing] Remove duplicated printing function.

1 files changed, 25 insertions, 0 deletions

diff --git a/printing/miscprint.ml b/printing/miscprint.ml
index 360843711c..a4ecbdf5e5 100644
--- a/printing/miscprint.ml
+++ b/printing/miscprint.ml
@@ -47,3 +47,28 @@ let pr_move_location pr_id = function
   | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
   | MoveFirst -> str " at top"
   | MoveLast -> str " at bottom"
+
+(** Printing of bindings *)
+let pr_binding prc = function
+  | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
+  | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+
+let pr_bindings prc prlc = function
+  | ImplicitBindings l ->
+    brk (1,1) ++ str "with" ++ brk (1,1) ++
+    pr_sequence prc l
+  | ExplicitBindings l ->
+    brk (1,1) ++ str "with" ++ brk (1,1) ++
+    pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+  | NoBindings -> mt ()
+
+let pr_bindings_no_with prc prlc = function
+  | ImplicitBindings l ->
+    brk (0,1) ++ prlist_with_sep spc prc l
+  | ExplicitBindings l ->
+    brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
+  | NoBindings -> mt ()
+
+let pr_with_bindings prc prlc (c,bl) =
+  hov 1 (prc c ++ pr_bindings prc prlc bl)
+