diff options
Diffstat (limited to 'tactics/extraargs.ml4')
| -rw-r--r-- | tactics/extraargs.ml4 | 35 |
1 files changed, 13 insertions, 22 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 6a13ac2a..58f07a1b 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -33,23 +33,9 @@ END 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() - in aux l -ARGUMENT EXTEND int_nelist - PRINTED BY pr_int_list_full - RAW_TYPED AS int list - RAW_PRINTED BY pr_int_list_full - GLOB_TYPED AS 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 () () () +let pr_int_list = Util.pr_sequence Pp.int +let pr_int_list_full _prc _prlc _prt l = pr_int_list l open Glob_term @@ -72,6 +58,8 @@ let interp_occs ist gl l = | ArgVar (_,id as locid) -> (try int_list_of_VList (List.assoc id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) +let interp_occs ist gl l = + Tacmach.project gl , interp_occs ist gl l let glob_occs ist l = l @@ -93,7 +81,7 @@ ARGUMENT EXTEND occurrences GLOB_TYPED AS occurrences_or_var GLOB_PRINTED BY pr_occurrences -| [ int_nelist(l) ] -> [ ArgArg l ] +| [ ne_integer_list(l) ] -> [ ArgArg l ] | [ var(id) ] -> [ ArgVar id ] END @@ -103,7 +91,7 @@ let pr_gen prc _prlc _prtac c = prc c let pr_globc _prc _prlc _prtac (_,glob) = Printer.pr_glob_constr glob -let interp_glob ist gl (t,_) = (ist,t) +let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) let glob_glob = Tacinterp.intern_constr @@ -150,6 +138,9 @@ let interp_place ist gl = function ConclLocation () -> ConclLocation () | HypLocation (id,hl) -> HypLocation (interp_hyp ist gl id,hl) +let interp_place ist gl p = + Tacmach.project gl , interp_place ist gl p + let subst_place subst pl = pl ARGUMENT EXTEND hloc @@ -287,13 +278,13 @@ let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x) (* spiwack argument for the commands of the retroknowledge *) let (wit_r_nat_field, globwit_r_nat_field, rawwit_r_nat_field) = - Genarg.create_arg "r_nat_field" + Genarg.create_arg None "r_nat_field" let (wit_r_n_field, globwit_r_n_field, rawwit_r_n_field) = - Genarg.create_arg "r_n_field" + Genarg.create_arg None "r_n_field" let (wit_r_int31_field, globwit_r_int31_field, rawwit_r_int31_field) = - Genarg.create_arg "r_int31_field" + Genarg.create_arg None "r_int31_field" let (wit_r_field, globwit_r_field, rawwit_r_field) = - Genarg.create_arg "r_field" + Genarg.create_arg None "r_field" (* spiwack: the print functions are incomplete, but I don't know what they are used for *) |