diff options
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 351 |
1 files changed, 242 insertions, 109 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index cb7d9b9c02..3bc9f2aa09 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -84,6 +84,32 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> Pp.t) -> 'a -> Pp.t +type 'a raw_extra_genarg_printer_with_level = + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a glob_extra_genarg_printer_with_level = + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + tolerability -> 'a -> Pp.t + +type 'a extra_genarg_printer_with_level = + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + tolerability -> 'a -> Pp.t + +let string_of_genarg_arg (ArgumentType arg) = + let rec aux : type a b c. (a, b, c) genarg_type -> string = function + | ListArg t -> aux t ^ "_list" + | OptArg t -> aux t ^ "_opt" + | PairArg (t1, t2) -> assert false (* No parsing/printing rule for it *) + | ExtraArg s -> ArgT.repr s in + aux arg + let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) @@ -116,7 +142,13 @@ type 'a extra_genarg_printer = | Val.Base t -> begin match Val.eq t tag with | None -> default - | Some Refl -> Genprint.generic_top_print (in_gen (Topwit wit) x) + | Some Refl -> + let open Genprint in + match generic_top_print (in_gen (Topwit wit) x) with + | TopPrinterBasic pr -> pr () + | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty + | TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } -> + printer (Global.env()) Evd.empty default_ensure_surrounded end | _ -> default @@ -129,7 +161,7 @@ type 'a extra_genarg_printer = (keyword "eval" ++ brk (1,1) ++ pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++ keyword "in" ++ spc() ++ prc c) - | ConstrContext ((_,id),c) -> + | ConstrContext ({CAst.v=id},c) -> hov 0 (keyword "context" ++ spc () ++ pr_id id ++ spc () ++ str "[ " ++ prlc c ++ str " ]") @@ -321,9 +353,10 @@ type 'a extra_genarg_printer = let rec strip_ty acc n ty = match ty.CAst.v with Constrexpr.CProdN(bll,a) -> - let nb = - List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in - let bll = List.map (fun (x, _, y) -> x, y) bll in + let bll = List.map (function + | CLocalAssum (nal,_,t) -> nal,t + | _ -> user_err Pp.(str "Cannot translate fix tactic: not only products")) bll in + let nb = List.fold_left (fun i (nal,t) -> i + List.length nal) 0 bll in if nb >= n then (List.rev (bll@acc)), a else strip_ty (bll@acc) (n-nb) a | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in @@ -331,12 +364,12 @@ type 'a extra_genarg_printer = let pr_ltac_or_var pr = function | ArgArg x -> pr x - | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id) + | ArgVar {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id) let pr_ltac_constant kn = if !Flags.in_debugger then KerName.print kn else try - pr_qualid (Nametab.shortest_qualid_of_tactic kn) + pr_qualid (Tacenv.shortest_qualid_of_tactic kn) with Not_found -> (* local tactic not accessible anymore *) str "<" ++ KerName.print kn ++ str ">" @@ -371,7 +404,7 @@ type 'a extra_genarg_printer = let pr_as_name = function | Anonymous -> mt () - | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.tag id) + | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (CAst.make id) let pr_pose_as_style prc na c = spc() ++ prc c ++ pr_as_name na @@ -432,12 +465,13 @@ type 'a extra_genarg_printer = let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs) - let pr_clauses default_is_concl pr_id = function + (* Some true = default is concl; Some false = default is all; None = no default *) + let pr_clauses has_default pr_id = function | { onhyps=Some []; concl_occs=occs } - when (match default_is_concl with Some true -> true | _ -> false) -> + when (match has_default with Some true -> true | _ -> false) -> pr_with_occurrences mt (occs,()) | { onhyps=None; concl_occs=AllOccurrences } - when (match default_is_concl with Some false -> true | _ -> false) -> mt () + when (match has_default with Some false -> true | _ -> false) -> mt () | { onhyps=None; concl_occs=NoOccurrences } -> pr_in (str " * |-") | { onhyps=None; concl_occs=occs } -> @@ -462,12 +496,12 @@ type 'a extra_genarg_printer = let pr_core_destruction_arg prc prlc = function | ElimOnConstr c -> pr_with_bindings prc prlc c - | ElimOnIdent (loc,id) -> pr_with_comments ?loc (pr_id id) + | ElimOnIdent {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id) | ElimOnAnonHyp n -> int n let pr_destruction_arg prc prlc (clear_flag,h) = pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h - + let pr_inversion_kind = function | SimpleInversion -> primitive "simple inversion" | FullInversion -> primitive "inversion" @@ -477,12 +511,14 @@ type 'a extra_genarg_printer = if Int.equal i j then int i else int i ++ str "-" ++ int j - let pr_goal_selector = function - | SelectNth i -> int i ++ str ":" - | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ - str "]" ++ str ":" - | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" - | SelectAll -> str "all" ++ str ":" +let pr_goal_selector toplevel = function + | SelectNth i -> int i ++ str ":" + | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":" + | SelectId id -> str "[" ++ Id.print id ++ str "]:" + | SelectAll -> assert toplevel; str "all:" + +let pr_goal_selector ~toplevel s = + (if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s let pr_lazy = function | General -> keyword "multi" @@ -491,11 +527,9 @@ type 'a extra_genarg_printer = let pr_match_pattern pr_pat = function | Term a -> pr_pat a - | Subterm (b,None,a) -> - (** ppedrot: we don't make difference between [appcontext] and [context] - anymore, and the interpretation is governed by a flag instead. *) + | Subterm (None,a) -> keyword "context" ++ str" [ " ++ pr_pat a ++ str " ]" - | Subterm (b,Some id,a) -> + | Subterm (Some id,a) -> keyword "context" ++ spc () ++ pr_id id ++ str "[ " ++ pr_pat a ++ str " ]" let pr_match_hyps pr_pat = function @@ -527,15 +561,24 @@ type 'a extra_genarg_printer = let pr_funvar n = spc () ++ Name.print n - let pr_let_clause k pr (id,(bl,t)) = - hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ - str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) - - let pr_let_clauses recflag pr = function + let pr_let_clause k pr_gen pr_arg (na,(bl,t)) = + let pr = function + | TacGeneric arg -> + let name = string_of_genarg_arg (genarg_tag arg) in + if name = "unit" || name = "int" then + (* Hard-wired parsing rules *) + pr_gen arg + else + str name ++ str ":" ++ surround (pr_gen arg) + | _ -> pr_arg (TacArg (Loc.tag t)) in + hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ + str " :=" ++ brk (1,1) ++ pr t) + + let pr_let_clauses recflag pr_gen pr = function | hd::tl -> hv 0 - (pr_let_clause (if recflag then "let rec" else "let") pr hd ++ - prlist (fun t -> spc () ++ pr_let_clause "with" pr t) tl) + (pr_let_clause (if recflag then "let rec" else "let") pr_gen pr hd ++ + prlist (fun t -> spc () ++ pr_let_clause "with" pr_gen pr t) tl) | [] -> anomaly (Pp.str "LetIn must declare at least one binding.") let pr_seq_body pr tl = @@ -641,7 +684,7 @@ type 'a extra_genarg_printer = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) - let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in spc() ++ hov 1 (str"(" ++ s ++ str")") in let pr_fix_tac (id,n,c) = @@ -649,10 +692,10 @@ type 'a extra_genarg_printer = (nal,ty)::bll -> if n <= List.length nal then match List.chop (n-1) nal with - _, (_,Name id) :: _ -> id, (nal,ty)::bll - | bef, (loc,Anonymous) :: aft -> + _, {CAst.v=Name id} :: _ -> id, (nal,ty)::bll + | bef, {CAst.loc;v=Anonymous} :: aft -> let id = next_ident_away (Id.of_string"y") avoid in - id, ((bef@(loc,Name id)::aft, ty)::bll) + id, ((bef@(CAst.make ?loc @@ Name id)::aft, ty)::bll) | _ -> assert false else let (id,bll') = set_nth_name avoid (n-List.length nal) bll in @@ -662,14 +705,14 @@ type 'a extra_genarg_printer = let names = List.fold_left (fun ln (nal,_) -> List.fold_left - (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln) + (fun ln na -> match na with { CAst.v=Name id } -> Id.Set.add id ln | _ -> ln) ln nal) - [] bll in + Id.Set.empty bll in let idarg,bll = set_nth_name names n bll in - let annot = match names with - | [_] -> + let annot = + if Int.equal (Id.Set.cardinal names) 1 then mt () - | _ -> + else spc() ++ str"{" ++ keyword "struct" ++ spc () ++ pr_id idarg ++ str"}" @@ -697,8 +740,10 @@ type 'a extra_genarg_printer = | TacIntroPattern (ev,[]) as t -> pr_atom0 t | TacIntroPattern (ev,(_::_ as p)) -> - hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++ - prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) + hov 1 (primitive (if ev then "eintros" else "intros") ++ + (match p with + | [_,Misctypes.IntroForthcoming false] -> mt () + | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( (if a then mt() else primitive "simple ") ++ @@ -849,7 +894,7 @@ type 'a extra_genarg_printer = let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in v 0 (hv 0 ( - pr_let_clauses recflag (pr_tac ltop) llc + pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc ++ spc () ++ keyword "in" ) ++ fnl () ++ pr_tac (llet,E) u), llet @@ -988,13 +1033,13 @@ type 'a extra_genarg_printer = keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet | TacComplete t -> pr_tac (lcomplete,E) t, lcomplete - | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom + | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom | TacId l -> keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom | TacAtom (loc,t) -> pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom | TacArg(_,Tacexp e) -> - pr.pr_tactic (latom,E) e, latom + pr_tac inherited e, latom | TacArg(_,ConstrMayEval (ConstrTerm c)) -> keyword "constr:" ++ pr.pr_constr c, latom | TacArg(_,ConstrMayEval c) -> @@ -1040,9 +1085,9 @@ type 'a extra_genarg_printer = let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else - match ty.CAst.v with + match DAst.get ty with Glob_term.GProd(na,Explicit,a,b) -> - strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b + strip_ty (([CAst.make na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty @@ -1111,10 +1156,10 @@ type 'a extra_genarg_printer = let ty = EConstr.Unsafe.to_constr ty in let rec strip_ty acc n ty = if n=0 then (List.rev acc, EConstr.of_constr ty) else - match Term.kind_of_term ty with - Term.Prod(na,a,b) -> - strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b - | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in + match Constr.kind ty with + | Constr.Prod(na,a,b) -> + strip_ty (([CAst.make na],EConstr.of_constr a)::acc) (n-1) b + | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty let pr_atomic_tactic_level env sigma n t = @@ -1166,95 +1211,183 @@ let declare_extra_genarg_pprule wit | ExtraArg s -> () | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") end; - let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in + let f x = + Genprint.PrinterBasic (fun () -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in let g x = + Genprint.PrinterBasic (fun () -> let env = Global.env () in - g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x) in let h x = + Genprint.TopPrinterNeedsContext (fun env sigma -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x) + in + Genprint.register_print0 wit f g h + +let declare_extra_genarg_pprule_with_level wit + (f : 'a raw_extra_genarg_printer_with_level) + (g : 'b glob_extra_genarg_printer_with_level) + (h : 'c extra_genarg_printer_with_level) default_surrounded default_non_surrounded = + begin match wit with + | ExtraArg s -> () + | _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.") + end; + let open Genprint in + let f x = + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in + let g x = let env = Global.env () in - h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x + PrinterNeedsLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun n -> + g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) n x) } + in + let h x = + TopPrinterNeedsContextAndLevel { + default_already_surrounded = default_surrounded; + default_ensure_surrounded = default_non_surrounded; + printer = (fun env sigma n -> + h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") n x) } in Genprint.register_print0 wit f g h +let declare_extra_vernac_genarg_pprule wit f = + let f x = Genprint.PrinterBasic (fun () -> f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in + Genprint.register_vernac_print0 wit f + (** Registering *) -let run_delayed c = c (Global.env ()) Evd.empty +let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma -> + let print_constr c = let (sigma, c) = c env sigma in pr_econstr_env env sigma c in + Miscprint.pr_intro_pattern print_constr p) + +let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma -> + pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma, + pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r) + +let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> + let sigma, bl = bl env sigma in + Miscprint.pr_bindings + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) + +let pr_with_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma -> + let sigma, bl = bl env sigma in + pr_with_bindings + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) bl) + +let pr_destruction_arg_env c = Genprint.TopPrinterNeedsContext (fun env sigma -> + let sigma, c = match c with + | clear_flag,ElimOnConstr g -> let sigma,c = g env sigma in sigma,(clear_flag,ElimOnConstr c) + | clear_flag,ElimOnAnonHyp n as x -> sigma, x + | clear_flag,ElimOnIdent id as x -> sigma, x in + pr_destruction_arg + (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c) + +let make_constr_printer f c = + Genprint.TopPrinterNeedsContextAndLevel { + Genprint.default_already_surrounded = Ppconstr.ltop; + Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr; + Genprint.printer = (fun env sigma n -> f env sigma n c)} -let run_delayed_destruction_arg = function (* HH: Using Evd.empty looks suspicious *) - | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (snd (run_delayed g)) - | clear_flag,ElimOnAnonHyp n as x -> x - | clear_flag,ElimOnIdent id as x -> x +let lift f a = Genprint.PrinterBasic (fun () -> f a) +let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a) + +let register_basic_print0 wit f g h = + Genprint.register_print0 wit (lift f) (lift g) (lift_top h) + + +let pr_glob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_glob_constr_env env c + +let pr_lglob_constr_pptac c = + let _, env = Pfedit.get_current_context () in + pr_lglob_constr_env env c let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in - let pr_string s = str "\"" ++ str s ++ str "\"" in - Genprint.register_print0 wit_int_or_var - (pr_or_var int) (pr_or_var int) int; - Genprint.register_print0 wit_ref + let open Genprint in + register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; + register_basic_print0 wit_ref pr_reference (pr_or_var (pr_located pr_global)) pr_global; - Genprint.register_print0 wit_ident - pr_id pr_id pr_id; - Genprint.register_print0 wit_var - (pr_located pr_id) (pr_located pr_id) pr_id; - Genprint.register_print0 + register_basic_print0 wit_ident pr_id pr_id pr_id; + register_basic_print0 wit_var pr_lident pr_lident pr_id; + register_print0 wit_intro_pattern - (Miscprint.pr_intro_pattern pr_constr_expr) - (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_econstr (snd (run_delayed c)))); + (lift (Miscprint.pr_intro_pattern pr_constr_expr)) + (lift (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac c))) + pr_intro_pattern_env; Genprint.register_print0 wit_clause_dft_concl - (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) pr_lident) - (pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id))) + (lift (pr_clauses (Some true) pr_lident)) + (lift (pr_clauses (Some true) pr_lident)) + (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (CAst.make id)) c)) ; Genprint.register_print0 wit_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) - Printer.pr_econstr + (lift Ppconstr.pr_lconstr_expr) + (lift (fun (c, _) -> pr_lglob_constr_pptac c)) + (make_constr_printer Printer.pr_econstr_n_env) ; Genprint.register_print0 wit_uconstr - Ppconstr.pr_constr_expr - (fun (c,_) -> Printer.pr_glob_constr c) - Printer.pr_closed_glob + (lift Ppconstr.pr_constr_expr) + (lift (fun (c,_) -> pr_glob_constr_pptac c)) + (make_constr_printer Printer.pr_closed_glob_n_env) ; Genprint.register_print0 wit_open_constr - Ppconstr.pr_constr_expr - (fun (c, _) -> Printer.pr_glob_constr c) - Printer.pr_econstr + (lift Ppconstr.pr_constr_expr) + (lift (fun (c, _) -> pr_glob_constr_pptac c)) + (make_constr_printer Printer.pr_econstr_n_env) + ; + Genprint.register_print0 + wit_red_expr + (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))) + (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) + pr_red_expr_env + ; + register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; + register_print0 wit_bindings + (lift (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr)) + (lift (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) + pr_bindings_env + ; + register_print0 wit_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) + pr_with_bindings_env + ; + register_print0 wit_open_constr_with_bindings + (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr)) + (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) + pr_with_bindings_env + ; + register_print0 Tacarg.wit_destruction_arg + (lift (pr_destruction_arg pr_constr_expr pr_lconstr_expr)) + (lift (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac))) + pr_destruction_arg_env ; - Genprint.register_print0 wit_red_expr - (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr)) - (pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr)) - (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern)); - Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis; - Genprint.register_print0 wit_bindings - (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr) - (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> Miscprint.pr_bindings_no_with pr_econstr pr_leconstr (snd (run_delayed it))); - Genprint.register_print0 wit_constr_with_bindings - (pr_with_bindings pr_constr_expr pr_lconstr_expr) - (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_with_bindings pr_econstr pr_leconstr (snd (run_delayed it))); - Genprint.register_print0 Tacarg.wit_destruction_arg - (pr_destruction_arg pr_constr_expr pr_lconstr_expr) - (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_destruction_arg pr_econstr pr_leconstr (run_delayed_destruction_arg it)); - Genprint.register_print0 Stdarg.wit_int int int int; - Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; - Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; - Genprint.register_print0 Stdarg.wit_pre_ident str str str; - Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string + register_basic_print0 Stdarg.wit_int int int int; + register_basic_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; + register_basic_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; + register_basic_print0 Stdarg.wit_pre_ident str str str; + register_basic_print0 Stdarg.wit_string qstring qstring qstring let () = - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_tactic printer printer printer + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_tactic printer printer printer + ltop (0,E) let () = - let pr_unit _ _ _ () = str "()" in - let printer _ _ prtac = prtac (0, E) in - declare_extra_genarg_pprule wit_ltac printer printer pr_unit + let pr_unit _ _ _ _ () = str "()" in + let printer _ _ prtac = prtac in + declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit + ltop (0,E) |