diff options
author | 2010-07-21 09:46:51 +0200 | |
---|---|---|
committer | 2010-07-21 09:46:51 +0200 | |
commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /parsing/pptactic.mli | |
parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) |
Imported Upstream snapshot 8.3~beta0+13298
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 |