From 14155762a7cd46ed6a3e9cf2a58e11ee1244b188 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 1 Jun 2016 18:31:05 +0200
Subject: [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`

This is what has always been used, so it doesn't represent a functional
change.

This is just a preliminary patch, but many more possibilities could be
done wrt tags.
---
 plugins/ltac/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 9dacce28d5..d9410a0885 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -43,7 +43,7 @@ struct
 
 end
 
-let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
+let tag t s = Pp.tag t s
 let do_not_tag _ x = x
 let tag_keyword                 = tag Tag.keyword
 let tag_primitive               = tag Tag.primitive
-- 
cgit v1.2.3