diff options
| author | Pierre-Marie Pédrot | 2016-01-14 23:34:52 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-16 13:33:03 +0100 |
| commit | 28ac569f0f8a0ae27552e4e4c20fc06ce12c720d (patch) | |
| tree | cde053a11fe0070e0a42065c79d1980bf5dd064a /grammar | |
| parent | 448866f0ec5291d58677d8fccbefde493ade0ee2 (diff) | |
Tactic notation printing accesses all the token data.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 12 |
1 files changed, 4 insertions, 8 deletions
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 |