diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-08-03 16:22:31 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-08-03 16:22:31 +0000 |
| commit | 94dc873f932681ead5031ca70ad96f33d8a636a1 (patch) | |
| tree | 73019bdd616ae8e7b0e803bebe6fb193543a1a4c /tactics/extraargs.mli | |
| parent | aab16ea645fefd71b6bd0fdb155a076640ab0d4e (diff) | |
Export printing functions for extra arguments. Maybe there's a way to
get them from the grammar entries?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13369 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/extraargs.mli')
| -rw-r--r-- | tactics/extraargs.mli | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index a59053cb1..f27642678 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -17,14 +17,17 @@ open Rawterm val rawwit_orient : bool raw_abstract_argument_type val wit_orient : bool typed_abstract_argument_type val orient : bool Pcoq.Gram.entry +val pr_orient : bool -> Pp.std_ppcmds val occurrences : (int list or_var) Pcoq.Gram.entry val rawwit_occurrences : (int list or_var) raw_abstract_argument_type val wit_occurrences : (int list) typed_abstract_argument_type +val pr_occurrences : int list Rawterm.or_var -> Pp.std_ppcmds val rawwit_raw : constr_expr raw_abstract_argument_type val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type val raw : constr_expr Pcoq.Gram.entry +val pr_raw : (Tacinterp.interp_sign * Rawterm.rawconstr) -> Pp.std_ppcmds type 'id gen_place= ('id * hyp_location_flag,unit) location @@ -34,19 +37,21 @@ type place = identifier gen_place val rawwit_hloc : loc_place raw_abstract_argument_type val wit_hloc : place typed_abstract_argument_type val hloc : loc_place Pcoq.Gram.entry - +val pr_hloc : loc_place -> Pp.std_ppcmds val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.entry val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Tacticals.clause - +val pr_in_arg_hyp : (Names.identifier list option * bool) -> Pp.std_ppcmds val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry val rawwit_by_arg_tac : raw_tactic_expr option raw_abstract_argument_type val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type - +val pr_by_arg_tac : + (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) -> + raw_tactic_expr option -> Pp.std_ppcmds (** Spiwack: Primitive for retroknowledge registration *) |