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 /printing/pptactic.mli | |
| parent | 448866f0ec5291d58677d8fccbefde493ade0ee2 (diff) | |
Tactic notation printing accesses all the token data.
Diffstat (limited to 'printing/pptactic.mli')
| -rw-r--r-- | printing/pptactic.mli | 6 |
1 files changed, 3 insertions, 3 deletions
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 |