diff options
| author | Pierre-Marie Pédrot | 2016-04-25 12:34:34 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-25 12:35:27 +0200 |
| commit | 76992bd0bab4d5b59e19d7a6a21c091f1c5d8340 (patch) | |
| tree | de075b506538c43a66f199f1403ea0a67536d0c1 | |
| parent | a7917a32b24b652d2978a7aea171aa01da37eece (diff) | |
Removing dead code related to printing of ML tactics in Pptactic.
| -rw-r--r-- | printing/pptactic.ml | 15 | ||||
| -rw-r--r-- | printing/pptactic.mli | 1 |
2 files changed, 0 insertions, 16 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 19536d9f83..631cb4c577 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -33,16 +33,9 @@ type pp_tactic = { pptac_prods : grammar_terminals; } -(* ML Extensions *) -let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t = - Hashtbl.create 17 - (* Tactic notations *) let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty -let declare_ml_tactic_pprule key pt = - Hashtbl.add prtac_tab key pt - let declare_notation_tactic_pprule kn pt = prnotation_tab := KNmap.add kn pt !prnotation_tab @@ -371,14 +364,6 @@ module Make pr_sequence (fun x -> x) l let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l = - try - let pp_rules = Hashtbl.find prtac_tab s in - let pp = pp_rules.(i) in - let args = List.map_filter filter_arg pp.pptac_prods in - let () = if not (List.for_all2eq check args l) then raise Not_found in - let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in - if pp.pptac_level > lev then surround p else p - with Not_found -> let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++ str "@" ++ int i diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 31a5a5d4a8..1608cae751 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -48,7 +48,6 @@ type pp_tactic = { pptac_prods : grammar_terminals; } -val declare_ml_tactic_pprule : ml_tactic_name -> pp_tactic array -> unit val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit (** The default pretty-printers produce {!Pp.std_ppcmds} that are |