1 files changed, 188 insertions, 190 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 7e903d2d3..c00036bb3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -26,21 +26,22 @@ open Printer
 
 let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
-type grammar_terminals = string option list
+type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list
 
 type pp_tactic = {
-  pptac_args : argument_type list;
-  pptac_prods : int * grammar_terminals;
+  pptac_level : int;
+  pptac_prods : grammar_terminals;
 }
 
 (* ML Extensions *)
-let prtac_tab = Hashtbl.create 17
+let prtac_tab : (ml_tactic_name, pp_tactic array) Hashtbl.t =
+  Hashtbl.create 17
 
 (* Tactic notations *)
 let prnotation_tab = Summary.ref ~name:"pptactic-notation" KNmap.empty
 
 let declare_ml_tactic_pprule key pt =
-  Hashtbl.add prtac_tab (key, pt.pptac_args) pt.pptac_prods
+  Hashtbl.add prtac_tab key pt
 
 let declare_notation_tactic_pprule kn pt =
   prnotation_tab := KNmap.add kn pt !prnotation_tab
@@ -264,149 +265,89 @@ module Make
   let with_evars ev s = if ev then "e" ^ s else s
 
 
-  let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generic_argument) =
-    match Genarg.genarg_tag x with
-      | IntOrVarArgType -> pr_or_var int (out_gen (rawwit wit_int_or_var) x)
-      | IdentArgType -> pr_id (out_gen (rawwit wit_ident) x)
-      | VarArgType -> pr_located pr_id (out_gen (rawwit wit_var) x)
-      | GenArgType -> pr_raw_generic prc prlc prtac prpat prref (out_gen (rawwit wit_genarg) x)
-      | ConstrArgType -> prc (out_gen (rawwit wit_constr) x)
-      | ConstrMayEvalArgType ->
-        pr_may_eval prc prlc (pr_or_by_notation prref) prpat
-          (out_gen (rawwit wit_constr_may_eval) x)
-      | QuantHypArgType -> pr_quantified_hypothesis (out_gen (rawwit wit_quant_hyp) x)
-      | RedExprArgType ->
-        pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
-          (out_gen (rawwit wit_red_expr) x)
-      | OpenConstrArgType -> prc (snd (out_gen (rawwit wit_open_constr) x))
-      | ConstrWithBindingsArgType ->
-        pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
-      | BindingsArgType ->
-        pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
-      | ListArgType _ ->
-        let list_unpacker wit l =
-          let map x = pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
-          pr_sequence map (raw l)
-        in
-        hov 0 (list_unpack { list_unpacker } x)
-      | OptArgType _ ->
-        let opt_unpacker wit o = match raw o with
+  let rec pr_raw_generic_rec prc prlc prtac prpat prref (GenArg (Rawwit wit, x)) =
+    match wit with
+      | ListArg wit ->
+        let map x = pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x) in
+        let ans = pr_sequence map x in
+        hov 0 ans
+      | OptArg wit ->
+        let ans = match x with
           | None -> mt ()
-          | Some x -> pr_raw_generic prc prlc prtac prpat prref (in_gen (rawwit wit) x)
-        in
-        hov 0 (opt_unpack { opt_unpacker } x)
-      | PairArgType _ ->
-        let pair_unpacker wit1 wit2 o =
-          let p, q = raw o in
-          let p = in_gen (rawwit wit1) p in
-          let q = in_gen (rawwit wit2) q in
-          pr_sequence (pr_raw_generic prc prlc prtac prpat prref) [p; q]
+          | Some x -> pr_raw_generic_rec prc prlc prtac prpat prref (in_gen (rawwit wit) x)
         in
-        hov 0 (pair_unpack { pair_unpacker } x)
-      | ExtraArgType s ->
-        try pi1 (String.Map.find s !genarg_pprule) prc prlc prtac x
-        with Not_found -> Genprint.generic_raw_print x
-
-
-  let rec pr_glb_generic prc prlc prtac prpat x =
-    match Genarg.genarg_tag x with
-      | IntOrVarArgType -> pr_or_var int (out_gen (glbwit wit_int_or_var) x)
-      | IdentArgType -> pr_id (out_gen (glbwit wit_ident) x)
-      | VarArgType -> pr_located pr_id (out_gen (glbwit wit_var) x)
-      | GenArgType -> pr_glb_generic prc prlc prtac prpat (out_gen (glbwit wit_genarg) x)
-      | ConstrArgType -> prc (out_gen (glbwit wit_constr) x)
-      | ConstrMayEvalArgType ->
-        pr_may_eval prc prlc
-          (pr_or_var (pr_and_short_name pr_evaluable_reference)) prpat
-          (out_gen (glbwit wit_constr_may_eval) x)
-      | QuantHypArgType ->
-        pr_quantified_hypothesis (out_gen (glbwit wit_quant_hyp) x)
-      | RedExprArgType ->
-        pr_red_expr
-          (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
-          (out_gen (glbwit wit_red_expr) x)
-      | OpenConstrArgType -> prc (snd (out_gen (glbwit wit_open_constr) x))
-      | ConstrWithBindingsArgType ->
-        pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
-      | BindingsArgType ->
-        pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
-      | ListArgType _ ->
-        let list_unpacker wit l =
-          let map x = pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x) in
-          pr_sequence map (glb l)
-        in
-        hov 0 (list_unpack { list_unpacker } x)
-      | OptArgType _ ->
-        let opt_unpacker wit o = match glb o with
+        hov 0 ans
+      | PairArg (wit1, wit2) ->
+        let p, q = x in
+        let p = in_gen (rawwit wit1) p in
+        let q = in_gen (rawwit wit2) q in
+        hov 0 (pr_sequence (pr_raw_generic_rec prc prlc prtac prpat prref) [p; q])
+      | ExtraArg s ->
+        try pi1 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (rawwit wit) x)
+        with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x)
+
+
+  let rec pr_glb_generic_rec prc prlc prtac prpat (GenArg (Glbwit wit, x)) =
+    match wit with
+      | ListArg wit ->
+        let map x = pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x) in
+        let ans = pr_sequence map x in
+        hov 0 ans
+      | OptArg wit ->
+        let ans = match x with
           | None -> mt ()
-          | Some x -> pr_glb_generic prc prlc prtac prpat (in_gen (glbwit wit) x)
-        in
-        hov 0 (opt_unpack { opt_unpacker } x)
-      | PairArgType _ ->
-        let pair_unpacker wit1 wit2 o =
-          let p, q = glb o in
-          let p = in_gen (glbwit wit1) p in
-          let q = in_gen (glbwit wit2) q in
-          pr_sequence (pr_glb_generic prc prlc prtac prpat) [p; q]
+          | Some x -> pr_glb_generic_rec prc prlc prtac prpat (in_gen (glbwit wit) x)
         in
-        hov 0 (pair_unpack { pair_unpacker } x)
-      | ExtraArgType s ->
-        try pi2 (String.Map.find s !genarg_pprule) prc prlc prtac x
-        with Not_found -> Genprint.generic_glb_print x
-
-  let rec pr_top_generic prc prlc prtac prpat x =
-    match Genarg.genarg_tag x with
-      | IntOrVarArgType -> pr_or_var int (out_gen (topwit wit_int_or_var) x)
-      | IdentArgType -> pr_id (out_gen (topwit wit_ident) x)
-      | VarArgType -> pr_id (out_gen (topwit wit_var) x)
-      | GenArgType -> pr_top_generic prc prlc prtac prpat (out_gen (topwit wit_genarg) x)
-      | ConstrArgType -> prc (out_gen (topwit wit_constr) x)
-      | ConstrMayEvalArgType -> prc (out_gen (topwit wit_constr_may_eval) x)
-      | QuantHypArgType -> pr_quantified_hypothesis (out_gen (topwit wit_quant_hyp) x)
-      | RedExprArgType ->
-        pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
-          (out_gen (topwit wit_red_expr) x)
-      | OpenConstrArgType -> prc (snd (out_gen (topwit wit_open_constr) x))
-      | ConstrWithBindingsArgType ->
-        let (c,b) = (out_gen (topwit wit_constr_with_bindings) x).Evd.it in
-        pr_with_bindings prc prlc (c,b)
-      | BindingsArgType ->
-        pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
-      | ListArgType _ ->
-        let list_unpacker wit l =
-          let map x = pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x) in
-          pr_sequence map (top l)
-        in
-        hov 0 (list_unpack { list_unpacker } x)
-      | OptArgType _ ->
-        let opt_unpacker wit o = match top o with
+        hov 0 ans
+      | PairArg (wit1, wit2) ->
+        let p, q = x in
+        let p = in_gen (glbwit wit1) p in
+        let q = in_gen (glbwit wit2) q in
+        let ans = pr_sequence (pr_glb_generic_rec prc prlc prtac prpat) [p; q] in
+        hov 0 ans
+      | ExtraArg s ->
+        try pi2 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (glbwit wit) x)
+        with Not_found -> Genprint.generic_glb_print (in_gen (glbwit wit) x)
+
+  let rec pr_top_generic_rec prc prlc prtac prpat (GenArg (Topwit wit, x)) =
+    match wit with
+      | ListArg wit ->
+        let map x = pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x) in
+        let ans = pr_sequence map x in
+        hov 0 ans
+      | OptArg wit ->
+        let ans = match x with
           | None -> mt ()
-          | Some x -> pr_top_generic prc prlc prtac prpat (in_gen (topwit wit) x)
-        in
-        hov 0 (opt_unpack { opt_unpacker } x)
-      | PairArgType _ ->
-        let pair_unpacker wit1 wit2 o =
-          let p, q = top o in
-          let p = in_gen (topwit wit1) p in
-          let q = in_gen (topwit wit2) q in
-          pr_sequence (pr_top_generic prc prlc prtac prpat) [p; q]
+          | Some x -> pr_top_generic_rec prc prlc prtac prpat (in_gen (topwit wit) x)
         in
-        hov 0 (pair_unpack { pair_unpacker } x)
-      | ExtraArgType s ->
-        try pi3 (String.Map.find s !genarg_pprule) prc prlc prtac x
-        with Not_found -> Genprint.generic_top_print x
+        hov 0 ans
+      | PairArg (wit1, wit2) ->
+        let p, q = x in
+        let p = in_gen (topwit wit1) p in
+        let q = in_gen (topwit wit2) q in
+        let ans = pr_sequence (pr_top_generic_rec prc prlc prtac prpat) [p; q] in
+        hov 0 ans
+      | ExtraArg s ->
+        try pi3 (String.Map.find (ArgT.repr s) !genarg_pprule) prc prlc prtac (in_gen (topwit wit) x)
+        with Not_found -> Genprint.generic_top_print (in_gen (topwit wit) x)
 
   let rec tacarg_using_rule_token pr_gen = function
-    | Some s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
-    | None :: l, a :: al ->
+    | Egramml.GramTerminal s :: l, al -> keyword s :: tacarg_using_rule_token pr_gen (l,al)
+    | Egramml.GramNonTerminal _ :: l, a :: al ->
       let r = tacarg_using_rule_token pr_gen (l,al) in
       pr_gen a :: r
     | [], [] -> []
     | _ -> failwith "Inconsistent arguments of extended tactic"
 
+  type any_arg = AnyArg : 'a Genarg.raw_abstract_argument_type -> any_arg
+
+  let filter_arg = function
+  | Egramml.GramTerminal _ -> None
+  | Egramml.GramNonTerminal (_, t, _) -> Some (AnyArg t)
+
   let pr_tacarg_using_rule pr_gen l =
     let l = match l with
-    | (Some s :: l, al) ->
+    | (Egramml.GramTerminal s :: l, al) ->
       (** First terminal token should be considered as the name of the tactic,
           so we tag it differently than the other terminal tokens. *)
       primitive s :: (tacarg_using_rule_token pr_gen (l, al))
@@ -414,42 +355,54 @@ module Make
     in
     pr_sequence (fun x -> x) l
 
-  let pr_extend_gen pr_gen lev s l =
+  let pr_extend_gen check pr_gen lev { mltac_name = s; mltac_index = i } l =
     try
-      let tags = List.map genarg_tag l in
-      let (lev',pl) = Hashtbl.find prtac_tab (s,tags) in
-      let p = pr_tacarg_using_rule pr_gen (pl,l) in
-      if lev' > lev then surround p else p
+      let pp_rules = Hashtbl.find prtac_tab s in
+      let pp = pp_rules.(i) in
+      let args = List.map_filter filter_arg pp.pptac_prods in
+      let () = if not (List.for_all2eq check args l) then raise Not_found in
+      let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in
+      if pp.pptac_level > lev then surround p else p
     with Not_found ->
-      let name = str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic in
+      let name =
+        str s.mltac_plugin ++ str "::" ++ str s.mltac_tactic ++
+        str "@" ++ int i
+      in
       let args = match l with
         | [] -> mt ()
         | _ -> spc() ++ pr_sequence pr_gen l
       in
       str "<" ++ name ++ str ">" ++ args
 
-  let pr_alias_gen pr_gen lev key l =
+  let pr_alias_gen check pr_gen lev key l =
     try
       let pp = KNmap.find key !prnotation_tab in
-      let (lev', pl) = pp.pptac_prods in
-      let p = pr_tacarg_using_rule pr_gen (pl, l) in
-      if lev' > lev then surround p else p
+      let args = List.map_filter filter_arg pp.pptac_prods in
+      let () = if not (List.for_all2eq check args l) then raise Not_found in
+      let p = pr_tacarg_using_rule pr_gen (pp.pptac_prods, l) in
+      if pp.pptac_level > lev then surround p else p
     with Not_found ->
       KerName.print key ++ spc() ++ pr_sequence pr_gen l ++ str" (* Generic printer *)"
 
-  let pr_raw_extend prc prlc prtac prpat =
-    pr_extend_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
-  let pr_glob_extend prc prlc prtac prpat =
-    pr_extend_gen (pr_glb_generic prc prlc prtac prpat)
-  let pr_extend prc prlc prtac prpat =
-    pr_extend_gen (pr_top_generic prc prlc prtac prpat)
+  let check_type t arg = match t, arg with
+  | AnyArg t, TacGeneric arg -> argument_type_eq (unquote t) (genarg_tag arg)
+  | _ -> false
+
+  let unwrap_gen f = function TacGeneric x -> f x | _ -> assert false
+
+  let pr_raw_extend_rec prc prlc prtac prpat =
+    pr_extend_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference))
+  let pr_glob_extend_rec prc prlc prtac prpat =
+    pr_extend_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat))
+  let pr_extend_rec prc prlc prtac prpat =
+    pr_extend_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat))
 
   let pr_raw_alias prc prlc prtac prpat =
-    pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference)
+    pr_alias_gen check_type (unwrap_gen (pr_raw_generic_rec prc prlc prtac prpat pr_reference))
   let pr_glob_alias prc prlc prtac prpat =
-    pr_alias_gen (pr_glb_generic prc prlc prtac prpat)
+    pr_alias_gen check_type (unwrap_gen (pr_glb_generic_rec prc prlc prtac prpat))
   let pr_alias prc prlc prtac prpat =
-    pr_alias_gen (pr_top_generic prc prlc prtac prpat)
+    pr_alias_gen check_type (unwrap_gen (pr_top_generic_rec prc prlc prtac prpat))
 
   (**********************************************************************)
   (* The tactic printer                                                 *)
@@ -716,11 +669,6 @@ module Make
     | l -> spc () ++
       hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l)
 
-  let string_of_debug = function
-    | Off -> ""
-    | Debug -> "debug "
-    | Info -> "info_"
-
   let pr_then () = str ";"
 
   let ltop = (5,E)
@@ -755,8 +703,8 @@ module Make
     pr_reference : 'ref -> std_ppcmds;
     pr_name      : 'nam -> std_ppcmds;
     pr_generic   : 'lev generic_argument -> std_ppcmds;
-    pr_extend    : int -> ml_tactic_name -> 'lev generic_argument list -> std_ppcmds;
-    pr_alias     : int -> KerName.t -> 'lev generic_argument list -> std_ppcmds;
+    pr_extend    : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds;
+    pr_alias     : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds;
   }
 
   constraint 'a = <
@@ -843,8 +791,6 @@ module Make
         let rec pr_atom0 a = tag_atom a (match a with
           | TacIntroPattern [] -> primitive "intros"
           | TacIntroMove (None,MoveLast) -> primitive "intro"
-          | TacTrivial (d,[],Some []) -> str (string_of_debug d) ++ primitive "trivial"
-          | TacAuto (d,None,[],Some []) -> str (string_of_debug d) ++ primitive "auto"
           | TacClear (true,[]) -> primitive "clear"
           | t -> str "(" ++ pr_atom1 t ++ str ")"
         )
@@ -953,23 +899,6 @@ module Make
               ++ pr_arg pr_quantified_hypothesis h2
             )
 
-          (* Automation tactics *)
-          | TacTrivial (_,[],Some []) as x ->
-            pr_atom0 x
-          | TacTrivial (d,lems,db) ->
-            hov 0 (
-              str (string_of_debug d) ++ primitive "trivial"
-              ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
-            )
-          | TacAuto (_,None,[],Some []) as x ->
-            pr_atom0 x
-          | TacAuto (d,n,lems,db) ->
-            hov 0 (
-              str (string_of_debug d) ++ primitive "auto"
-              ++ pr_opt (pr_or_var int) n
-              ++ pr_auto_using pr.pr_constr lems ++ pr_hintbases db
-            )
-
           (* Context management *)
           | TacClear (true,[]) as t ->
             pr_atom0 t
@@ -1251,16 +1180,13 @@ module Make
             | TacML (loc,s,l) ->
               pr_with_comments loc (pr.pr_extend 1 s l), lcall
             | TacAlias (loc,kn,l) ->
-              pr_with_comments loc (pr.pr_alias (level_of inherited) kn (List.map snd l)), latom
+              pr_with_comments loc (pr.pr_alias (level_of inherited) kn l), latom
           )
           in
           if prec_less prec inherited then strm
           else str"(" ++ strm ++ str")"
 
         and pr_tacarg = function
-          | TacDynamic (loc,t) ->
-            pr_with_comments loc
-              (str "<" ++ keyword "dynamic" ++ str " [" ++ str (Dyn.tag t) ++ str "]>")
           | MetaIdArg (loc,true,s) ->
             pr_with_comments loc (str "$" ++ str s)
           | MetaIdArg (loc,false,s) ->
@@ -1307,7 +1233,7 @@ module Make
       pr_reference = pr_reference;
       pr_name = pr_lident;
       pr_generic = Genprint.generic_raw_print;
-      pr_extend = pr_raw_extend pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
+      pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
       pr_alias = pr_raw_alias pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr;
     } in
     make_pr_tac
@@ -1321,7 +1247,7 @@ module Make
 
   let pr_pat_and_constr_expr pr ((c,_),_) = pr c
 
-  let rec pr_glob_tactic_level env n t =
+  let pr_glob_tactic_level env n t =
     let glob_printers =
       (strip_prod_binders_glob_constr)
     in
@@ -1338,7 +1264,7 @@ module Make
         pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
         pr_name = pr_lident;
         pr_generic = Genprint.generic_glb_print;
-        pr_extend = pr_glob_extend
+        pr_extend = pr_glob_extend_rec
           (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
           prtac (pr_pat_and_constr_expr (pr_glob_constr_env env));
         pr_alias = pr_glob_alias
@@ -1374,13 +1300,13 @@ module Make
         pr_uconstr = pr_closed_glob_env env Evd.empty;
         pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
         pr_lconstr = pr_lconstr_env env Evd.empty;
-        pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
-        pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
-        pr_constant = pr_and_short_name (pr_evaluable_reference_env env);
+        pr_pattern = pr_constr_pattern_env env Evd.empty;
+        pr_lpattern = pr_lconstr_pattern_env env Evd.empty;
+        pr_constant = pr_evaluable_reference_env env;
         pr_reference = pr_located pr_ltac_constant;
         pr_name = pr_id;
         pr_generic = Genprint.generic_top_print;
-        pr_extend = pr_extend
+        pr_extend = pr_extend_rec
           (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
           (pr_glob_tactic_level env) pr_constr_pattern;
         pr_alias = pr_alias
@@ -1395,6 +1321,39 @@ module Make
     in
     prtac n t
 
+  let pr_raw_generic env = pr_raw_generic_rec
+    pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr pr_reference
+
+  let pr_glb_generic env = pr_glb_generic_rec
+    (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+    (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+
+  let pr_top_generic env = pr_top_generic_rec
+    (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
+    (pr_glob_tactic_level env) pr_constr_pattern
+
+  let pr_raw_extend env = pr_raw_extend_rec
+    pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr
+
+  let pr_glob_extend env = pr_glob_extend_rec
+    (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env))
+    (pr_glob_tactic_level env) (pr_pat_and_constr_expr (pr_glob_constr_env env))
+
+  let check_val_type t arg =
+    let AnyArg t = t in
+(*     let t = Genarg.val_tag (Obj.magic t) in *)
+(*     let Val.Dyn (t', _) = arg in *)
+(*     match Genarg.Val.eq t t' with *)
+(*     | None -> false *)
+(*     | Some _ -> true *)
+    true (** FIXME *)
+
+  let pr_alias pr lev key args =
+    pr_alias_gen check_val_type pr lev key args
+
+  let pr_extend pr lev ml args =
+    pr_extend_gen check_val_type pr lev ml args
+
   let pr_tactic env = pr_tactic_level env ltop
 
 end
@@ -1431,17 +1390,26 @@ end)
 
 (** Registering *)
 
+let run_delayed c =
+  Sigma.run Evd.empty { Sigma.run = fun sigma -> c.delayed (Global.env ()) sigma }
+
 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 Constrarg.wit_int_or_var
+    (pr_or_var int) (pr_or_var int) int;
   Genprint.register_print0 Constrarg.wit_ref
     pr_reference (pr_or_var (pr_located pr_global)) pr_global;
+  Genprint.register_print0 Constrarg.wit_ident
+    pr_id pr_id pr_id;
+  Genprint.register_print0 Constrarg.wit_var
+    (pr_located pr_id) (pr_located pr_id) pr_id;
   Genprint.register_print0
     Constrarg.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_constr (snd (c (Global.env()) Evd.empty))));
+    (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c))));
   Genprint.register_print0
     Constrarg.wit_clause_dft_concl
     (pr_clauses (Some true) pr_lident)
@@ -1451,11 +1419,41 @@ let () =
   Genprint.register_print0 Constrarg.wit_sort
     pr_glob_sort pr_glob_sort (pr_sort Evd.empty);
   Genprint.register_print0
+    Constrarg.wit_constr
+    Ppconstr.pr_constr_expr
+    (fun (c, _) -> Printer.pr_glob_constr c)
+    Printer.pr_constr
+  ;
+  Genprint.register_print0
     Constrarg.wit_uconstr
     Ppconstr.pr_constr_expr
     (fun (c,_) -> Printer.pr_glob_constr c)
     Printer.pr_closed_glob
   ;
+  Genprint.register_print0
+    Constrarg.wit_open_constr
+    Ppconstr.pr_constr_expr
+    (fun (c, _) -> Printer.pr_glob_constr c)
+    Printer.pr_constr
+  ;
+  Genprint.register_print0 Constrarg.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_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
+    (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern));
+  Genprint.register_print0 Constrarg.wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
+  Genprint.register_print0 Constrarg.wit_bindings
+    (pr_bindings_no_with pr_constr_expr pr_lconstr_expr)
+    (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr))
+    (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it)));
+  Genprint.register_print0 Constrarg.wit_constr_may_eval
+    (pr_may_eval pr_constr_expr pr_lconstr_expr (pr_or_by_notation pr_reference) pr_constr_pattern_expr)
+    (pr_may_eval (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_constr;
+  Genprint.register_print0 Constrarg.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_constr pr_lconstr (fst (run_delayed 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;