From b5e90d92fc52e568f1ed6e65a4b611bdab80e8f5 Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Wed, 7 Jun 2017 15:44:41 +0200
Subject: completing a sentence in a comment

---
 lib/pp.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index 7a191b01a..45834dade 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -13,6 +13,7 @@
 (* `Pp.t` or `Pp.std_ppcmds` is the main pretty printing document type  *)
 (* in the Coq system. Documents are composed laying out boxes, and      *)
 (* users can add arbitrary tag metadata that backends are free          *)
+(* to interpret.                                                        *)
 (*                                                                      *)
 (* The datatype has a public view to allow serialization or advanced    *)
 (* uses, however regular users are _strongly_ warned againt its use,    *)
-- 
cgit v1.2.3