diff options
| author | herbelin | 2003-09-18 17:15:32 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-18 17:15:32 +0000 |
| commit | 25b2bf4053c7c97f70c9dfef465f5eeb414fcaaa (patch) | |
| tree | 27af658873fe151a9a58839e8d49b260021f29c6 /parsing/pptactic.mli | |
| parent | a7d06e11179d5d96a98382add560ed399b96712b (diff) | |
Simplification afficheur de tactiques non primitive
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4408 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pptactic.mli')
| -rw-r--r-- | parsing/pptactic.mli | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 5d5f62f389..729947bb8e 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -40,13 +40,11 @@ val declare_extra_genarg_pprule : ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) -> ('b closed_abstract_argument_type * 'b extra_genarg_printer) -> unit -type ('a,'b) gen_gram_prod_builder = - ('a,'b) generic_argument list -> - string * Egrammar.grammar_tactic_production list +type grammar_terminals = string option list (* if the boolean is false then the extension applies only to old syntax *) -val declare_extra_tactic_pprule : - bool -> string -> ('a,'b) gen_gram_prod_builder -> unit +val declare_extra_tactic_pprule : bool -> string -> + argument_type list * (string * grammar_terminals) -> unit val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds |