diff options
| -rw-r--r-- | ltac/tacentries.ml | 19 |
1 files changed, 7 insertions, 12 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 91eaa85228..c4569b98f7 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -233,10 +233,6 @@ let interp_prod_item lev = function let EntryName (etyp, e) = interp_entry_name interp symbol in GramNonTerminal (loc, etyp, e) -let make_terminal_status = function - | GramTerminal s -> Some s - | GramNonTerminal _ -> None - let make_fresh_key = let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in fun () -> @@ -256,10 +252,14 @@ type tactic_grammar_obj = { tacobj_key : KerName.t; tacobj_local : locality_flag; tacobj_tacgram : tactic_grammar; - tacobj_tacpp : Pptactic.pp_tactic; tacobj_body : Id.t list * Tacexpr.glob_tactic_expr; } +let pprule pa = { + Pptactic.pptac_level = pa.tacgram_level; + pptac_prods = pa.tacgram_prods; +} + let check_key key = if Tacenv.check_alias key then error "Conflicting tactic notations keys. This can happen when including \ @@ -270,7 +270,7 @@ let cache_tactic_notation (_, tobj) = let () = check_key key in Tacenv.register_alias key tobj.tacobj_body; extend_tactic_grammar key tobj.tacobj_tacgram; - Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp + Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram) let open_tactic_notation i (_, tobj) = let key = tobj.tacobj_key in @@ -282,7 +282,7 @@ let load_tactic_notation i (_, tobj) = let () = check_key key in (** Only add the printing and interpretation rules. *) Tacenv.register_alias key tobj.tacobj_body; - Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp; + Pptactic.declare_notation_tactic_pprule key (pprule tobj.tacobj_tacgram); if Int.equal i 1 && not tobj.tacobj_local then extend_tactic_grammar key tobj.tacobj_tacgram @@ -310,10 +310,6 @@ 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 pprule = { - Pptactic.pptac_level = n; - pptac_prods = prods; - } in let tac = Tacintern.glob_tactic_env ids (Global.env()) e in let parule = { tacgram_level = n; @@ -323,7 +319,6 @@ let add_tactic_notation local n prods e = tacobj_key = make_fresh_key (); tacobj_local = local; tacobj_tacgram = parule; - tacobj_tacpp = pprule; tacobj_body = (ids, tac); } in Lib.add_anonymous_leaf (inTacticGrammar tacobj) |