From db9b17d55f539fcfda799a9fe15caa2530cc727f Mon Sep 17 00:00:00 2001
From: Regis-Gianas
Date: Tue, 4 Nov 2014 14:46:47 +0100
Subject: printing/Ppannotation: Introduce a new annotation for keywords.
 printing/{Ppconstr, Ppvernac}: Use it.

---
 printing/ppannotation.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'printing/ppannotation.mli')

diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
index 38b09eef0c..d10bc5a571 100644
--- a/printing/ppannotation.mli
+++ b/printing/ppannotation.mli
@@ -14,6 +14,7 @@ open Constrexpr
 open Vernacexpr
 
 type t =
+  | AKeyword
   | AUnparsing  of unparsing
   | AConstrExpr of constr_expr
   | AVernac     of vernac_expr
-- 
cgit v1.2.3