diff options
| author | ppedrot | 2012-10-04 11:53:19 +0000 |
|---|---|---|
| committer | ppedrot | 2012-10-04 11:53:19 +0000 |
| commit | 41abdd815f9384e197cba73ee67f2b78f89a6319 (patch) | |
| tree | 9b0d2b502e98e705529d1b244d0eaf8026f72f86 /printing/pptactic.ml | |
| 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/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index d16035fba0..b790c4ea68 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) |