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.mli | |
| 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.mli')
| -rw-r--r-- | printing/pptactic.mli | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 249a4a0afb..61acffd081 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 |