summaryrefslogtreecommitdiff
path: root/printing/pputils.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/pputils.ml')
-rw-r--r--printing/pputils.ml15
1 files changed, 15 insertions, 0 deletions
diff --git a/printing/pputils.ml b/printing/pputils.ml
new file mode 100644
index 00000000..ee1a39ef
--- /dev/null
+++ b/printing/pputils.ml
@@ -0,0 +1,15 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Pp
+
+let pr_located pr (loc, x) =
+ if Flags.do_beautify () && loc <> Loc.ghost then
+ let (b, e) = Loc.unloc loc in
+ Pp.comment b ++ pr x ++ Pp.comment e
+ else pr x