diff options
| author | Pierre-Marie Pédrot | 2016-04-25 16:22:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-04-25 16:26:35 +0200 |
| commit | cca1a283d4693ef75f2aa48fc07c4d51bcd108c7 (patch) | |
| tree | de075b506538c43a66f199f1403ea0a67536d0c1 /printing | |
| parent | 65578a55b81252e2c4b006728522839a9e37cd5c (diff) | |
| parent | 76992bd0bab4d5b59e19d7a6a21c091f1c5d8340 (diff) | |
Simplifying and uniformizing the implementation of tactic notations.
This branch mainly provides two features:
1. The resolution of tactic notation scopes is not tied to a hardwired Pcoq
registration anymore. We expose instead an API to interpret names as a given
generic argument, effectively reversing the logical dependency between parsing
entries and generic arguments.
2. ML tactics do not declare their own notation system anymore. They rely instead
on plain tactic notations, except for a little hack due to the way we currently
interpret toplevel values.
Diffstat (limited to 'printing')
| -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 |