Removing the ad-hoc tactic_expr type.

This type was actually only used by the debug printer of tactics, and only
for atomic tactics. Furthermore, that type was asymmetric, as the underlying
tacexpr type was set to be glob_tactic, when the semantics would have required
a Val.t type.

Furthermore, this type is absent from every contrib I have seen, which hints
again in favour of its lack of meaning.

8 files changed, 17 insertions, 50 deletions

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index f821251c27..875ad3d160 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -377,19 +377,13 @@ type t_dispatch =  <
     constant:t_cst;
     reference:t_ref;
     name:t_nam;
-    tacexpr:glob_tactic_expr;
+    tacexpr:unit;
     level:tlevel
 >
 
-type tactic_expr =
-    t_dispatch gen_tactic_expr
-
 type atomic_tactic_expr =
     t_dispatch gen_atomic_tactic_expr
 
-type tactic_arg =
-    t_dispatch gen_tactic_arg
-
 (** Misc *)
 
 type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 6f0297268d..02b03b72c2 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1650,7 +1650,7 @@ and name_atomic ?env tacexpr tac : unit Proofview.tactic =
   | Some e -> Proofview.tclUNIT e
   | None -> Proofview.tclENV
   end >>= fun env ->
-  let name () = Pptactic.pr_tactic env (TacAtom (Loc.ghost,tacexpr)) in
+  let name () = Pptactic.pr_atomic_tactic env tacexpr in
   Proofview.Trace.name_tactic name tac
 
 (* Interprets a primitive tactic *)
@@ -1769,7 +1769,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let tac = Option.map (interp_tactic ist) t in
         Tacticals.New.tclWITHHOLES false
         (name_atomic ~env
-          (TacAssert(b,t,ipat,c))
+          (TacAssert(b,Option.map ignore t,ipat,c))
           (Tactics.forward b tac ipat' c)) sigma
       end }
   | TacGeneralize cl ->
@@ -1951,7 +1951,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma = project gl in
         let cl = interp_clause ist env sigma cl in
         name_atomic ~env
-          (TacRewrite (ev,l,cl,by))
+          (TacRewrite (ev,l,cl,Option.map ignore by))
           (Equality.general_multi_rewrite ev l' cl
              (Option.map (fun by -> Tacticals.New.tclCOMPLETE (interp_tactic ist by),
                Equality.Naive)
diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index df7f925b73..511f93569c 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -20,7 +20,6 @@ type t =
   | AGlobAtomicTacticExpr of glob_atomic_tactic_expr
   | ARawTacticExpr        of raw_tactic_expr
   | ARawAtomicTacticExpr  of raw_atomic_tactic_expr
-  | ATacticExpr           of tactic_expr
   | AAtomicTacticExpr     of atomic_tactic_expr
 
 let tag_of_annotation = function
@@ -32,7 +31,6 @@ let tag_of_annotation = function
   | AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr"
   | ARawTacticExpr _        -> "raw_tactic_expr"
   | ARawAtomicTacticExpr _  -> "raw_atomic_tactic_expr"
-  | ATacticExpr _           -> "tactic_expr"
   | AAtomicTacticExpr _     -> "atomic_tactic_expr"
 
 let attributes_of_annotation a =
diff --git a/printing/ppannotation.mli b/printing/ppannotation.mli
index 84724053ed..a0fef1a757 100644
--- a/printing/ppannotation.mli
+++ b/printing/ppannotation.mli
@@ -23,7 +23,6 @@ type t =
   | AGlobAtomicTacticExpr of glob_atomic_tactic_expr
   | ARawTacticExpr        of raw_tactic_expr
   | ARawAtomicTacticExpr  of raw_atomic_tactic_expr
-  | ATacticExpr           of tactic_expr
   | AAtomicTacticExpr     of atomic_tactic_expr
 
 val tag_of_annotation : t -> string
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 1e6c46e759..3cff541b06 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -94,8 +94,6 @@ module Make
         : raw_tactic_expr -> std_ppcmds -> std_ppcmds
       val tag_raw_atomic_tactic_expr
         : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
-      val tag_tactic_expr
-        : tactic_expr -> std_ppcmds -> std_ppcmds
       val tag_atomic_tactic_expr
         : atomic_tactic_expr -> std_ppcmds -> std_ppcmds
   end)
@@ -411,15 +409,11 @@ module Make
     pr_extend_gen check_type (pr_farg prtac)
   let pr_glob_extend_rec prc prlc prtac prpat =
     pr_extend_gen check_type (pr_farg prtac)
-  let pr_extend_rec prc prlc prtac prpat =
-    pr_extend_gen check_type (pr_farg prtac)
 
   let pr_raw_alias prc prlc prtac prpat =
     pr_alias_gen check_type (pr_farg prtac)
   let pr_glob_alias prc prlc prtac prpat =
     pr_alias_gen check_type (pr_farg prtac)
-  let pr_alias prc prlc prtac prpat =
-    pr_alias_gen check_type (pr_farg prtac)
 
   (**********************************************************************)
   (* The tactic printer                                                 *)
@@ -528,9 +522,8 @@ module Make
     | ipat ->
       spc() ++ prc c ++ pr_as_ipat prdc ipat
 
-  let pr_by_tactic prt = function
-    | TacId [] -> mt ()
-    | tac -> spc() ++ keyword "by" ++ spc () ++ prt tac
+  let pr_by_tactic prt tac =
+    spc() ++ keyword "by" ++ spc () ++ prt tac
 
   let pr_hyp_location pr_id = function
     | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
@@ -732,7 +725,7 @@ module Make
       level     :'lev
     >
 
-    let rec pr_atom pr strip_prod_binders tag_atom =
+    let pr_atom pr strip_prod_binders tag_atom =
       let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
       let pr_with_bindings_arg_full = pr_with_bindings_arg in
       let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
@@ -1255,13 +1248,10 @@ module Make
           | _ -> error "Cannot translate fix tactic: not enough products" in
     strip_ty [] n ty
 
-  let pr_tactic_level env n t =
-    let typed_printers =
-      (strip_prod_binders_constr)
-    in
-    let rec prtac n (t:tactic_expr) =
+  let pr_atomic_tactic_level env n t =
+    let prtac n (t:atomic_tactic_expr) =
       let pr = {
-        pr_tactic = pr_glob_tactic_level env;
+        pr_tactic = (fun _ _ -> str "<tactic>");
         pr_constr = pr_constr_env env Evd.empty;
         pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
         pr_lconstr = pr_lconstr_env env Evd.empty;
@@ -1270,21 +1260,13 @@ module Make
         pr_constant = pr_evaluable_reference_env env;
         pr_reference = pr_located pr_ltac_constant;
         pr_name = pr_id;
-        pr_generic = pr_top_generic_rec
-          (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
-          pr_value pr_constr_pattern;
-        pr_extend = pr_extend_rec
-          (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
-          prtac pr_constr_pattern;
-        pr_alias = pr_alias
-          (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty)
-          prtac pr_constr_pattern;
+        (** Those are not used by the atomic printer *)
+        pr_generic = (fun _ -> assert false);
+        pr_extend = (fun _ _ _ -> assert false);
+        pr_alias = (fun _ _ _ -> assert false);
       }
       in
-      make_pr_tac
-        pr typed_printers
-        tag_atomic_tactic_expr tag_tactic_expr
-        n t
+      pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
     in
     prtac n t
 
@@ -1321,7 +1303,7 @@ module Make
   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
+  let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
 
 end
 
@@ -1351,7 +1333,6 @@ include Make (Ppconstr) (struct
     let tag_glob_atomic_tactic_expr = do_not_tag
     let tag_raw_tactic_expr         = do_not_tag
     let tag_raw_atomic_tactic_expr  = do_not_tag
-    let tag_tactic_expr             = do_not_tag
     let tag_atomic_tactic_expr      = do_not_tag
 end)
 
@@ -1449,7 +1430,6 @@ module Richpp = struct
     let tag_glob_atomic_tactic_expr a = tag (AGlobAtomicTacticExpr a)
     let tag_raw_tactic_expr         e = tag (ARawTacticExpr e)
     let tag_raw_atomic_tactic_expr  a = tag (ARawAtomicTacticExpr a)
-    let tag_tactic_expr             e = tag (ATacticExpr e)
     let tag_atomic_tactic_expr      a = tag (AAtomicTacticExpr a)
   end)
 
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 95cf541fd7..d4858bac4f 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -57,7 +57,7 @@ module type Pp = sig
 
   val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
 
-  val pr_tactic : env -> tactic_expr -> std_ppcmds
+  val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
 
   val pr_hintbases : string list option -> std_ppcmds
 
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
index d95e190749..5f39f36eab 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -22,4 +22,3 @@ let make_richpp pr ast =
 
 let richpp_vernac = make_richpp RichppVernac.pr_vernac
 let richpp_constr = make_richpp RichppConstr.pr_constr_expr
-let richpp_tactic env = make_richpp (RichppTactic.pr_tactic env)
diff --git a/printing/richprinter.mli b/printing/richprinter.mli
index 261d22c4c3..c9e84e3eb4 100644
--- a/printing/richprinter.mli
+++ b/printing/richprinter.mli
@@ -34,6 +34,3 @@ val richpp_vernac : Vernacexpr.vernac_expr -> rich_pp
 
 (** [richpp_constr constr] produces a rich pretty-printing of [constr]. *)
 val richpp_constr : Constrexpr.constr_expr -> rich_pp
-
-(** [richpp_tactic constr] produces a rich pretty-printing of [tactic]. *)
-val richpp_tactic : Environ.env -> Tacexpr.tactic_expr -> rich_pp