From 25b2bf4053c7c97f70c9dfef465f5eeb414fcaaa Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 18 Sep 2003 17:15:32 +0000
Subject: Simplification afficheur de tactiques non primitive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4408 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pptactic.mli | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'parsing/pptactic.mli')

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
 
-- 
cgit v1.2.3