diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extraargs.ml4 | 24 | ||||
| -rw-r--r-- | tactics/extraargs.mli | 11 |
2 files changed, 25 insertions, 10 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 0c8203bee..25a64c3dd 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -25,14 +25,15 @@ let pr_orient _prc _prlc _prt = function | true -> Pp.mt () | false -> Pp.str " <-" - ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient | [ "->" ] -> [ true ] | [ "<-" ] -> [ false ] | [ ] -> [ true ] END -let pr_int_list _prc _prlc _prt l = +let pr_orient = pr_orient () () () + +let pr_int_list_full _prc _prlc _prt l = let rec aux = function | i :: l -> Pp.int i ++ Pp.spc () ++ aux l | [] -> Pp.mt() @@ -40,20 +41,22 @@ let pr_int_list _prc _prlc _prt l = ARGUMENT EXTEND int_nelist TYPED AS int list - PRINTED BY pr_int_list + PRINTED BY pr_int_list_full RAW_TYPED AS int list - RAW_PRINTED BY pr_int_list + RAW_PRINTED BY pr_int_list_full GLOB_TYPED AS int list - GLOB_PRINTED BY pr_int_list + GLOB_PRINTED BY pr_int_list_full | [ integer(x) int_nelist(l) ] -> [x::l] | [ integer(x) ] -> [ [x] ] END +let pr_int_list = pr_int_list_full () () () + open Rawterm let pr_occurrences _prc _prlc _prt l = match l with - | ArgArg x -> pr_int_list _prc _prlc _prt x + | ArgArg x -> pr_int_list x | ArgVar (loc, id) -> Nameops.pr_id id let coerce_to_int = function @@ -80,7 +83,7 @@ type occurrences = int list ARGUMENT EXTEND occurrences TYPED AS occurrences - PRINTED BY pr_int_list + PRINTED BY pr_int_list_full INTERPRETED BY interp_occs GLOBALIZED BY glob_occs @@ -96,9 +99,12 @@ ARGUMENT EXTEND occurrences | [ var(id) ] -> [ ArgVar id ] END +let pr_occurrences = pr_occurrences () () () + let pr_gen prc _prlc _prtac c = prc c let pr_rawc _prc _prlc _prtac (_,raw) = Printer.pr_rawconstr raw +let pr_raw = pr_rawc () () () let interp_raw ist gl (t,_) = (ist,t) @@ -122,6 +128,7 @@ ARGUMENT EXTEND raw [ lconstr(c) ] -> [ c ] END + type 'id gen_place= ('id * hyp_location_flag,unit) location type loc_place = identifier Util.located gen_place @@ -137,6 +144,7 @@ let pr_gen_place pr_id = function let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Nameops.pr_id id) let pr_place _ _ _ = pr_gen_place Nameops.pr_id +let pr_hloc = pr_loc_place () () () let intern_place ist = function ConclLocation () -> ConclLocation () @@ -191,6 +199,7 @@ ARGUMENT EXTEND by_arg_tac | [ ] -> [ None ] END +let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c let pr_in_hyp pr_id (lo,concl) : Pp.std_ppcmds = match lo,concl with @@ -265,6 +274,7 @@ ARGUMENT EXTEND in_arg_hyp | [ ] -> [ (Some [],true) ] END +let pr_in_arg_hyp = pr_in_arg_hyp_typed () () () let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause = {Tacexpr.onhyps= 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 *) |