diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-04 11:53:19 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-04 11:53:19 +0000 |
| commit | 41abdd815f9384e197cba73ee67f2b78f89a6319 (patch) | |
| tree | 9b0d2b502e98e705529d1b244d0eaf8026f72f86 /printing | |
| parent | 5b6582f8d47975f6f4f394cf44a1c65c799d43ff (diff) | |
Adding a nominal typing layer to Metasyntax in order to clarify
things up. Records are used instead of their equivalents as tuples.
This is maybe syntactically heavier, but this is semantically
equivalent and easier to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15848 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 10 | ||||
| -rw-r--r-- | printing/pptactic.mli | 9 |
2 files changed, 15 insertions, 4 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index d16035fba..b790c4ea6 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -28,11 +28,17 @@ let pr_global x = Nametab.pr_global_env Idset.empty x type grammar_terminals = string option list +type pp_tactic = { + pptac_key : string; + pptac_args : argument_type list; + pptac_prods : int * grammar_terminals; +} + (* Extensions *) let prtac_tab = Hashtbl.create 17 -let declare_extra_tactic_pprule (s,tags,prods) = - Hashtbl.add prtac_tab (s,tags) prods +let declare_extra_tactic_pprule pt = + Hashtbl.add prtac_tab (pt.pptac_key, pt.pptac_args) (pt.pptac_prods) let exists_extra_tactic_pprule s tags = Hashtbl.mem prtac_tab (s,tags) diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 249a4a0af..61acffd08 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -47,9 +47,14 @@ val declare_extra_genarg_pprule : type grammar_terminals = string option list +type pp_tactic = { + pptac_key : string; + pptac_args : argument_type list; + pptac_prods : int * grammar_terminals; +} + (** if the boolean is false then the extension applies only to old syntax *) -val declare_extra_tactic_pprule : - string * argument_type list * (int * grammar_terminals) -> unit +val declare_extra_tactic_pprule : pp_tactic -> unit val exists_extra_tactic_pprule : string -> argument_type list -> bool |