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 /toplevel | |
| parent | 448866f0ec5291d58677d8fccbefde493ade0ee2 (diff) | |
Tactic notation printing accesses all the token data.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 6ba5f4f875..6919729fe9 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -55,11 +55,6 @@ let make_terminal_status = function | GramTerminal s -> Some s | GramNonTerminal _ -> None -let rec make_tags = function - | GramTerminal s :: l -> make_tags l - | GramNonTerminal (loc, etyp, _) :: l -> Genarg.unquote etyp :: make_tags l - | [] -> [] - let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in fun () -> @@ -133,10 +128,9 @@ let cons_production_parameter = function let add_tactic_notation (local,n,prods,e) = let ids = List.map_filter cons_production_parameter prods in let prods = List.map (interp_prod_item n) prods in - let tags = make_tags prods in let pprule = { - Pptactic.pptac_args = tags; - pptac_prods = (n, List.map make_terminal_status prods); + Pptactic.pptac_level = n; + pptac_prods = prods; } in let tac = Tacintern.glob_tactic_env ids (Global.env()) e in let parule = { |