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.

---
 grammar/tacextend.ml4 | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

(limited to 'grammar')

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index bf0c4fc215..a870722fdf 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -86,10 +86,6 @@ let rec make_args = function
       <:expr< [ Genarg.in_gen $make_topwit loc t$ $lid:p$ :: $make_args l$ ] >>
   | _::l -> make_args l
 
-let mlexpr_terminals_of_grammar_tactic_prod_item_expr = function
-  | ExtTerminal s -> <:expr< Some $mlexpr_of_string s$ >>
-  | ExtNonTerminal _ -> <:expr< None >>
-
 let make_prod_item = function
   | ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
   | ExtNonTerminal (EntryName (nt, g), id) ->
@@ -98,7 +94,7 @@ let make_prod_item = function
       $mlexpr_of_prod_entry_key g$ >>
 
 let mlexpr_of_clause cl =
-  mlexpr_of_list (fun (a,_,b) -> mlexpr_of_list make_prod_item a) cl
+  mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
 
 let rec make_tags loc = function
   | [] -> <:expr< [] >>
@@ -112,9 +108,9 @@ let rec make_tags loc = function
 let make_one_printing_rule (pt,_,e) =
   let level = mlexpr_of_int 0 in (* only level 0 supported here *)
   let loc = MLast.loc_of_expr e in
-  let prods = mlexpr_of_list mlexpr_terminals_of_grammar_tactic_prod_item_expr pt in
-  <:expr< { Pptactic.pptac_args = $make_tags loc pt$;
-            pptac_prods = ($level$, $prods$) } >>
+  let prods = mlexpr_of_list make_prod_item pt in
+  <:expr< { Pptactic.pptac_level = $level$;
+            pptac_prods = $prods$ } >>
 
 let make_printing_rule r = mlexpr_of_list make_one_printing_rule r
 
-- 
cgit v1.2.3