From 28ac569f0f8a0ae27552e4e4c20fc06ce12c720d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 Jan 2016 23:34:52 +0100
Subject: Tactic notation printing accesses all the token data.

---
 printing/pptactic.mli | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'printing/pptactic.mli')

diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 30b9483db7..57c7f67fd4 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -41,11 +41,11 @@ val declare_extra_genarg_pprule :
   'b glob_extra_genarg_printer ->
   'c extra_genarg_printer -> unit
 
-type grammar_terminals = string option list
+type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list
 
 type pp_tactic = {
-  pptac_args : argument_type list;
-  pptac_prods : int * grammar_terminals;
+  pptac_level : int;
+  pptac_prods : grammar_terminals;
 }
 
 val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit
-- 
cgit v1.2.3