diff options
Diffstat (limited to 'parsing/pptactic.mli')
| -rw-r--r-- | parsing/pptactic.mli | 33 |
1 files changed, 19 insertions, 14 deletions
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index e24f666f..446dc9f9 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pptactic.mli 11309 2008-08-06 10:30:35Z herbelin $ i*) +(*i $Id$ i*) open Pp open Genarg @@ -15,6 +15,7 @@ open Pretyping open Proof_type open Topconstr open Rawterm +open Pattern open Ppextend open Environ open Evd @@ -25,8 +26,8 @@ val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds type 'a raw_extra_genarg_printer = - (constr_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds @@ -37,13 +38,13 @@ type 'a glob_extra_genarg_printer = 'a -> std_ppcmds type 'a extra_genarg_printer = - (Term.constr -> std_ppcmds) -> - (Term.constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> 'a -> std_ppcmds (* if the boolean is false then the extension applies only to old syntax *) -val declare_extra_genarg_pprule : +val declare_extra_genarg_pprule : ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) -> ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) -> ('b typed_abstract_argument_type * 'b extra_genarg_printer) -> unit @@ -51,31 +52,35 @@ val declare_extra_genarg_pprule : type grammar_terminals = string option list (* if the boolean is false then the extension applies only to old syntax *) -val declare_extra_tactic_pprule : +val declare_extra_tactic_pprule : string * argument_type list * (int * grammar_terminals) -> unit val exists_extra_tactic_pprule : string -> argument_type list -> bool -val pr_raw_generic : +val pr_raw_generic : (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> (tolerability -> raw_tactic_expr -> std_ppcmds) -> - (Libnames.reference -> std_ppcmds) -> constr_expr generic_argument -> + (constr_expr -> std_ppcmds) -> + (Libnames.reference -> std_ppcmds) -> rlevel generic_argument -> std_ppcmds val pr_raw_extend: (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) -> - (tolerability -> raw_tactic_expr -> std_ppcmds) -> int -> + (tolerability -> raw_tactic_expr -> std_ppcmds) -> + (constr_expr -> std_ppcmds) -> int -> string -> raw_generic_argument list -> std_ppcmds val pr_glob_extend: (rawconstr_and_expr -> std_ppcmds) -> (rawconstr_and_expr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> int -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (rawconstr_pattern_and_expr -> std_ppcmds) -> int -> string -> glob_generic_argument list -> std_ppcmds val pr_extend : - (open_constr -> std_ppcmds) -> (open_constr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> int -> + (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> + (tolerability -> glob_tactic_expr -> std_ppcmds) -> + (constr_pattern -> std_ppcmds) -> int -> string -> typed_generic_argument list -> std_ppcmds val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds @@ -83,7 +88,7 @@ val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds - + val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds |