Revert "Taking into account the original grammar rule to print generic"

This reverts commit 043d6a5c113a11fe9955cbe71b8f4bcd08af9a90.

3 files changed, 11 insertions, 58 deletions

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c3c4009ca..f58452176 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -70,17 +70,6 @@ let declare_extra_genarg_pprule wit f g h =
   let h prc prlc prtac x = h prc prlc prtac (out_gen (topwit wit) x) in
   genarg_pprule := String.Map.add s (f,g,h) !genarg_pprule
 
-let find_extra_genarg_pprule wit =
-  let s = match wit with
-    | ExtraArg s -> ArgT.repr s
-    | _ -> error
-      "Can declare a pretty-printing rule only for extra argument types."
-  in
-  let (f,g,h) = String.Map.find s !genarg_pprule in
-  (fun prc prlc prtac x -> f prc prlc prtac (in_gen (rawwit wit) x)),
-  (fun prc prlc prtac x -> g prc prlc prtac (in_gen (glbwit wit) x)),
-  (fun prc prlc prtac x -> h prc prlc prtac (in_gen (topwit wit) x))
-
 module Make
   (Ppconstr : Ppconstrsig.Pp)
   (Taggers : sig
@@ -309,6 +298,7 @@ module Make
         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 ->
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 270f709b7..1608cae75 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -41,12 +41,6 @@ val declare_extra_genarg_pprule :
   'b glob_extra_genarg_printer ->
   'c extra_genarg_printer -> unit
 
-val find_extra_genarg_pprule :
-  ('a, 'b, 'c) genarg_type ->
-  'a raw_extra_genarg_printer *
-  'b glob_extra_genarg_printer *
-  'c extra_genarg_printer
-
 type grammar_terminals = Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list
 
 type pp_tactic = {
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index fb9dca255..efdaa366b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -21,7 +21,7 @@ open Decl_kinds
 
 module Make
   (Ppconstr : Ppconstrsig.Pp)
-  (Pptacticsig : Pptacticsig.Pp)
+  (Pptactic : Pptacticsig.Pp)
   (Taggers  : sig
     val tag_keyword : std_ppcmds -> std_ppcmds
     val tag_vernac  : vernac_expr -> std_ppcmds -> std_ppcmds
@@ -30,7 +30,7 @@ module Make
 
   open Taggers
   open Ppconstr
-  open Pptacticsig
+  open Pptactic
 
   let keyword s = tag_keyword (str s)
 
@@ -81,39 +81,11 @@ module Make
     | VernacEndSubproof -> str""
     | _ -> str"."
 
+  let pr_gen t = pr_raw_generic (Global.env ()) t
+
   let sep = fun _ -> spc()
   let sep_v2 = fun _ -> str"," ++ spc()
 
-  open Genarg
-
-  type 'c entry_name = EntryName : ('c, 'a) Extend.symbol -> 'c entry_name
-
-  let hov_if_not_empty n p = if Pp.ismt p then p else hov n p
-
-  let rec pr_gen = function
-    | GenArg (Rawwit (ListArg wit), x), EntryName (Alist1 e) ->
-        let map x = pr_gen (GenArg (rawwit wit, x), EntryName e) in
-        hov_if_not_empty 0 (pr_sequence map x)
-    | GenArg (Rawwit (ListArg wit), x), EntryName (Alist0 e) ->
-        let map x = pr_gen (GenArg (rawwit wit, x), EntryName e) in
-        hov_if_not_empty 0 (pr_sequence map x)
-    | GenArg (Rawwit (ListArg wit), x), EntryName (Alist1sep (e,sep)) ->
-        let map x = pr_gen (GenArg (rawwit wit, x), EntryName e) in
-        hov_if_not_empty 0 (prlist_with_sep (fun () -> spc() ++ str sep ++ spc()) map x)
-    | GenArg (Rawwit (ListArg wit), x), EntryName (Alist0sep (e,sep)) ->
-        let map x = pr_gen (GenArg (rawwit wit, x), EntryName e) in
-        hov_if_not_empty 0 (prlist_with_sep (fun () -> spc() ++ str sep ++ spc()) map x)
-    | GenArg (Rawwit (OptArg wit), x), EntryName (Aopt e) ->
-        let ans = match x with
-          | None -> mt ()
-          | Some x -> pr_gen (GenArg (rawwit wit, x), EntryName e) in
-        hov_if_not_empty 0 ans
-    | GenArg (Rawwit (PairArg (wit1, wit2)), _), _ -> error "Pair of entries not implemented."
-    | GenArg (Rawwit (ExtraArg s as wit), x), e ->
-        (try pi1 (Pptactic.find_extra_genarg_pprule wit) pr_constr_expr pr_lconstr_expr (fun _ -> pr_raw_tactic) x
-        with Not_found -> Genprint.generic_raw_print (in_gen (rawwit wit) x))
-    | _, _ -> assert false
-
   let pr_set_entry_type = function
     | ETName -> str"ident"
     | ETReference -> str"global"
@@ -1229,23 +1201,20 @@ module Make
         return (str "}")
 
   and pr_extend s cl =
-    let pr_based_on_grammar a =
+    let pr_arg a =
       try pr_gen a
       with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
-    let pr_based_on_structure a =
-      try Pptactic.pr_raw_generic (Global.env ()) a
-      with Failure _ -> str "<error in " ++ str (fst s) ++ str ">" in
     try
       let rl = Egramml.get_extend_vernac_rule s in
-      let rec aux sep rl cl =
+      let rec aux rl cl =
         match rl, cl with
-        | Egramml.GramNonTerminal (_,_,e) :: rl, (GenArg (wit,x)) :: cl -> pr_based_on_grammar (GenArg (wit,x),EntryName e) :: aux sep rl cl
-        | Egramml.GramTerminal s :: rl, cl -> sep() ++ str s :: aux spc rl cl
+        | Egramml.GramNonTerminal _ :: rl, arg :: cl -> pr_arg arg :: aux rl cl
+        | Egramml.GramTerminal s :: rl, cl -> str s :: aux rl cl
         | [], [] -> []
         | _ -> assert false in
-      hov 1 (pr_sequence (fun x -> x) (aux mt rl cl))
+      hov 1 (pr_sequence (fun x -> x) (aux rl cl))
     with Not_found ->
-      hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_based_on_structure cl ++ str ")")
+      hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
   let pr_vernac v =
     try pr_vernac_body v ++ sep_end v