1 files changed, 178 insertions, 91 deletions

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 38460c669f..fbb70cca68 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Pp
@@ -84,6 +86,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)
 
@@ -119,9 +147,9 @@ type 'a extra_genarg_printer =
           | Some Refl ->
              let open Genprint in
              match generic_top_print (in_gen (Topwit wit) x) with
-             | PrinterBasic pr -> pr ()
-             | PrinterNeedsContext pr -> pr (Global.env()) Evd.empty
-             | PrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
+             | 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
@@ -135,7 +163,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 " ]")
@@ -327,9 +355,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
@@ -337,7 +366,7 @@ 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
@@ -377,7 +406,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
@@ -469,12 +498,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"
@@ -500,11 +529,9 @@ let pr_goal_selector ~toplevel s =
 
   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
@@ -536,15 +563,24 @@ let pr_goal_selector ~toplevel s =
 
   let pr_funvar n = spc () ++ Name.print n
 
-  let pr_let_clause k pr (na,(bl,t)) =
+  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 (TacArg (Loc.tag t)))
+             str " :=" ++ brk (1,1) ++ pr t)
 
-  let pr_let_clauses recflag pr = function
+  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 =
@@ -650,7 +686,7 @@ let pr_goal_selector ~toplevel s =
         (*  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) =
@@ -658,10 +694,10 @@ let pr_goal_selector ~toplevel s =
         (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
@@ -671,7 +707,7 @@ let pr_goal_selector ~toplevel s =
         let names =
           List.fold_left
             (fun ln (nal,_) -> List.fold_left
-              (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln)
+              (fun ln na -> match na with { CAst.v=Name id } -> Id.Set.add id ln | _ -> ln)
               ln nal)
             Id.Set.empty bll in
         let idarg,bll = set_nth_name names n bll in
@@ -706,8 +742,10 @@ let pr_goal_selector ~toplevel s =
         | 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 ") ++
@@ -858,7 +896,7 @@ let pr_goal_selector ~toplevel s =
               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
@@ -1003,7 +1041,7 @@ let pr_goal_selector ~toplevel s =
             | 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) ->
@@ -1051,7 +1089,7 @@ let pr_goal_selector ~toplevel s =
       if Int.equal n 0 then (List.rev acc, (ty,None)) else
         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
 
@@ -1122,7 +1160,7 @@ let pr_goal_selector ~toplevel s =
       if n=0 then (List.rev acc, EConstr.of_constr ty) else
         match Constr.kind ty with
         | Constr.Prod(na,a,b) ->
-          strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) 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
 
@@ -1175,42 +1213,77 @@ 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.PrinterNeedsContext (fun env sigma ->
+    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
+    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 = 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
   Genprint.register_vernac_print0 wit f
 
 (** Registering *)
 
-let pr_intro_pattern_env p = Genprint.PrinterNeedsContext (fun env sigma ->
+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.PrinterNeedsContext (fun env sigma ->
+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.PrinterNeedsContext (fun env sigma ->
+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.PrinterNeedsContext (fun env sigma ->
+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.PrinterNeedsContext (fun env sigma ->
+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
@@ -1219,90 +1292,104 @@ let pr_destruction_arg_env c = Genprint.PrinterNeedsContext (fun env sigma ->
     (pr_econstr_env env sigma) (pr_leconstr_env env sigma) c)
 
 let make_constr_printer f c =
-  Genprint.PrinterNeedsContextAndLevel {
+  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 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
-  Genprint.register_print0 wit_int_or_var
-    (pr_or_var int) (pr_or_var int) (lift int);
-  Genprint.register_print0 wit_ref
-    pr_reference (pr_or_var (pr_located pr_global)) (lift pr_global);
-  Genprint.register_print0 wit_ident
-    pr_id pr_id (lift pr_id);
-  Genprint.register_print0 wit_var
-    (pr_located pr_id) (pr_located pr_id) (lift pr_id);
-  Genprint.register_print0
+  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;
+  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))
+    (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)
-    (fun c -> Genprint.PrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c))
+    (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)
+    (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)
+    (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)
+    (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
-    (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))
+  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
   ;
-  Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis (lift 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))
+  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
   ;
-  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))
+  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
   ;
-  Genprint.register_print0 wit_open_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))
+  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
   ;
-  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))
+  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 Stdarg.wit_int int int (lift int);
-  Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool (lift pr_bool);
-  Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit (lift pr_unit);
-  Genprint.register_print0 Stdarg.wit_pre_ident str str (lift str);
-  Genprint.register_print0 Stdarg.wit_string qstring qstring (lift qstring)
+  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)