Removing the typed-level tactic_expr type.

8 files changed, 250 insertions, 284 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 4b2dc49a5e..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,247 +725,246 @@ module Make
       level     :'lev
     >
 
-    let make_pr_tac pr strip_prod_binders tag_atom tag =
-
-        (* some shortcuts *)
-        let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in
-        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
-        let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
-
-        let pr_constrarg c = spc () ++ pr.pr_constr c in
-        let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
-        let pr_intarg n = spc () ++ int n in
-
-        (* Some printing combinators *)
-        let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in
+    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
+      let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
+
+      let pr_constrarg c = spc () ++ pr.pr_constr c in
+      let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
+      let pr_intarg n = spc () ++ int n in
+
+      (* Some printing combinators *)
+      let pr_eliminator cb = keyword "using" ++ pr_arg pr_with_bindings cb in
+
+      let pr_binder_fix (nal,t) =
+        (*  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
+        spc() ++ hov 1 (str"(" ++ s ++ str")") in
+
+      let pr_fix_tac (id,n,c) =
+        let rec set_nth_name avoid n = function
+        (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 ->
+                let id = next_ident_away (Id.of_string"y") avoid in
+                id, ((bef@(loc,Name id)::aft, ty)::bll)
+              | _ -> assert false
+          else
+            let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
+            (id,(nal,ty)::bll')
+          | [] -> assert false in
+        let (bll,ty) = strip_prod_binders n c in
+        let names =
+          List.fold_left
+            (fun ln (nal,_) -> List.fold_left
+              (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
+              ln nal)
+            [] bll in
+        let idarg,bll = set_nth_name names n bll in
+        let annot = match names with
+          | [_] ->
+            mt ()
+          | _ ->
+            spc() ++ str"{"
+            ++ keyword "struct" ++ spc ()
+            ++ pr_id idarg ++ str"}"
+        in
+        hov 1 (str"(" ++ pr_id id ++
+                  prlist pr_binder_fix bll ++ annot ++ str" :" ++
+                  pr_lconstrarg ty ++ str")") in
+      (*  spc() ++
+          hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+          c)
+      *)
+      let pr_cofix_tac (id,c) =
+        hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
+
+      (* Printing tactics as arguments *)
+      let rec pr_atom0 a = tag_atom a (match a with
+        | TacIntroPattern [] -> primitive "intros"
+        | TacIntroMove (None,MoveLast) -> primitive "intro"
+        | t -> str "(" ++ pr_atom1 t ++ str ")"
+      )
+
+      (* Main tactic printer *)
+      and pr_atom1 a = tag_atom a (match a with
+        (* Basic tactics *)
+        | TacIntroPattern [] as t ->
+          pr_atom0 t
+        | TacIntroPattern (_::_ as p) ->
+          hov 1 (primitive "intros" ++ spc () ++
+                    prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
+        | TacIntroMove (None,MoveLast) as t ->
+          pr_atom0 t
+        | TacIntroMove (Some id,MoveLast) ->
+          primitive "intro" ++ spc () ++ pr_id id
+        | TacIntroMove (ido,hto) ->
+          hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
+                    Miscprint.pr_move_location pr.pr_name hto)
+        | TacExact c ->
+          hov 1 (primitive "exact" ++ pr_constrarg c)
+        | TacApply (a,ev,cb,inhyp) ->
+          hov 1 (
+            (if a then mt() else primitive "simple ") ++
+              primitive (with_evars ev "apply") ++ spc () ++
+              prlist_with_sep pr_comma pr_with_bindings_arg cb ++
+              pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp
+          )
+        | TacElim (ev,cb,cbo) ->
+          hov 1 (
+            primitive (with_evars ev "elim")
+            ++ pr_arg pr_with_bindings_arg cb
+            ++ pr_opt pr_eliminator cbo)
+        | TacCase (ev,cb) ->
+          hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
+        | TacMutualFix (id,n,l) ->
+          hov 1 (
+            primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
+            ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
+        | TacMutualCofix (id,l) ->
+          hov 1 (
+            primitive "cofix" ++ spc () ++ pr_id id ++ spc()
+            ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
+          )
+        | TacAssert (b,Some tac,ipat,c) ->
+          hov 1 (
+            primitive (if b then "assert" else "enough") ++
+              pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
+              pr_by_tactic (pr.pr_tactic ltop) tac
+          )
+        | TacAssert (_,None,ipat,c) ->
+          hov 1 (
+            primitive "pose proof"
+            ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
+          )
+        | TacGeneralize l ->
+          hov 1 (
+            primitive "generalize" ++ spc ()
+            ++ prlist_with_sep pr_comma (fun (cl,na) ->
+              pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
+              l
+          )
+        | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
+          hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+        | TacLetTac (na,c,cl,b,e) ->
+          hov 1 (
+            (if b then primitive "set" else primitive "remember") ++
+              (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
+                else pr_pose_as_style pr.pr_constr na c) ++
+              pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
+              pr_non_empty_arg (pr_clauses (Some b) pr.pr_name) cl)
+        (*  | TacInstantiate (n,c,ConclLocation ()) ->
+            hov 1 (str "instantiate" ++ spc() ++
+            hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+            pr_lconstrarg c ++ str ")" ))
+            | TacInstantiate (n,c,HypLocation (id,hloc)) ->
+            hov 1 (str "instantiate" ++ spc() ++
+            hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+            pr_lconstrarg c ++ str ")" )
+            ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
+        *)
 
-        let extract_binders = function
-          | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
-          | body -> ([],body) in
+        (* Derived basic tactics *)
+        | TacInductionDestruct (isrec,ev,(l,el)) ->
+          hov 1 (
+            primitive (with_evars ev (if isrec then "induction" else "destruct"))
+            ++ spc ()
+            ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
+              pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
+                pr_with_induction_names pr.pr_dconstr ids ++
+                pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++
+              pr_opt pr_eliminator el
+          )
+        | TacDoubleInduction (h1,h2) ->
+          hov 1 (
+            primitive "double induction"
+            ++ pr_arg pr_quantified_hypothesis h1
+            ++ pr_arg pr_quantified_hypothesis h2
+          )
 
-        let pr_binder_fix (nal,t) =
-          (*  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
-          spc() ++ hov 1 (str"(" ++ s ++ str")") in
-
-        let pr_fix_tac (id,n,c) =
-          let rec set_nth_name avoid n = function
-          (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 ->
-                  let id = next_ident_away (Id.of_string"y") avoid in
-                  id, ((bef@(loc,Name id)::aft, ty)::bll)
-                | _ -> assert false
-            else
-              let (id,bll') = set_nth_name avoid (n-List.length nal) bll in
-              (id,(nal,ty)::bll')
-            | [] -> assert false in
-          let (bll,ty) = strip_prod_binders n c in
-          let names =
-            List.fold_left
-              (fun ln (nal,_) -> List.fold_left
-                (fun ln na -> match na with (_,Name id) -> id::ln | _ -> ln)
-                ln nal)
-              [] bll in
-          let idarg,bll = set_nth_name names n bll in
-          let annot = match names with
-            | [_] ->
-              mt ()
-            | _ ->
-              spc() ++ str"{"
-              ++ keyword "struct" ++ spc ()
-              ++ pr_id idarg ++ str"}"
-          in
-          hov 1 (str"(" ++ pr_id id ++
-                   prlist pr_binder_fix bll ++ annot ++ str" :" ++
-                   pr_lconstrarg ty ++ str")") in
-        (*  spc() ++
-            hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
-            c)
-        *)
-        let pr_cofix_tac (id,c) =
-          hov 1 (str"(" ++ pr_id id ++ str" :" ++ pr_lconstrarg c ++ str")") in
-
-        (* Printing tactics as arguments *)
-        let rec pr_atom0 a = tag_atom a (match a with
-          | TacIntroPattern [] -> primitive "intros"
-          | TacIntroMove (None,MoveLast) -> primitive "intro"
-          | t -> str "(" ++ pr_atom1 t ++ str ")"
-        )
-
-        (* Main tactic printer *)
-        and pr_atom1 a = tag_atom a (match a with
-          (* Basic tactics *)
-          | TacIntroPattern [] as t ->
-            pr_atom0 t
-          | TacIntroPattern (_::_ as p) ->
-            hov 1 (primitive "intros" ++ spc () ++
-                     prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)
-          | TacIntroMove (None,MoveLast) as t ->
-            pr_atom0 t
-          | TacIntroMove (Some id,MoveLast) ->
-            primitive "intro" ++ spc () ++ pr_id id
-          | TacIntroMove (ido,hto) ->
-            hov 1 (primitive "intro" ++ pr_opt pr_id ido ++
-                     Miscprint.pr_move_location pr.pr_name hto)
-          | TacExact c ->
-            hov 1 (primitive "exact" ++ pr_constrarg c)
-          | TacApply (a,ev,cb,inhyp) ->
-            hov 1 (
-              (if a then mt() else primitive "simple ") ++
-                primitive (with_evars ev "apply") ++ spc () ++
-                prlist_with_sep pr_comma pr_with_bindings_arg cb ++
-                pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp
-            )
-          | TacElim (ev,cb,cbo) ->
-            hov 1 (
-              primitive (with_evars ev "elim")
-              ++ pr_arg pr_with_bindings_arg cb
-              ++ pr_opt pr_eliminator cbo)
-          | TacCase (ev,cb) ->
-            hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb)
-          | TacMutualFix (id,n,l) ->
-            hov 1 (
-              primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc()
-              ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l)
-          | TacMutualCofix (id,l) ->
-            hov 1 (
-              primitive "cofix" ++ spc () ++ pr_id id ++ spc()
-              ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
-            )
-          | TacAssert (b,Some tac,ipat,c) ->
-            hov 1 (
-              primitive (if b then "assert" else "enough") ++
-                pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
-                pr_by_tactic (pr.pr_tactic ltop) tac
-            )
-          | TacAssert (_,None,ipat,c) ->
-            hov 1 (
-              primitive "pose proof"
-              ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
-            )
-          | TacGeneralize l ->
-            hov 1 (
-              primitive "generalize" ++ spc ()
-              ++ prlist_with_sep pr_comma (fun (cl,na) ->
-                pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
-                l
-            )
-          | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
-            hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
-          | TacLetTac (na,c,cl,b,e) ->
-            hov 1 (
-              (if b then primitive "set" else primitive "remember") ++
-                (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
-                 else pr_pose_as_style pr.pr_constr na c) ++
-                pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
-                pr_non_empty_arg (pr_clauses (Some b) pr.pr_name) cl)
-          (*  | TacInstantiate (n,c,ConclLocation ()) ->
-              hov 1 (str "instantiate" ++ spc() ++
-              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
-              pr_lconstrarg c ++ str ")" ))
-              | TacInstantiate (n,c,HypLocation (id,hloc)) ->
-              hov 1 (str "instantiate" ++ spc() ++
-              hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
-              pr_lconstrarg c ++ str ")" )
-              ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None)))
-          *)
-
-          (* Derived basic tactics *)
-          | TacInductionDestruct (isrec,ev,(l,el)) ->
-            hov 1 (
-              primitive (with_evars ev (if isrec then "induction" else "destruct"))
-              ++ spc ()
-              ++ prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) ->
-                pr_clear_flag clear_flag (pr_induction_arg pr.pr_dconstr pr.pr_dconstr) h ++
-                  pr_with_induction_names pr.pr_dconstr ids ++
-                  pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++
-                pr_opt pr_eliminator el
-            )
-          | TacDoubleInduction (h1,h2) ->
-            hov 1 (
-              primitive "double induction"
-              ++ pr_arg pr_quantified_hypothesis h1
-              ++ pr_arg pr_quantified_hypothesis h2
-            )
+        (* Context management *)
+        | TacRename l ->
+          hov 1 (
+            primitive "rename" ++ brk (1,1)
+            ++ prlist_with_sep
+              (fun () -> str "," ++ brk (1,1))
+              (fun (i1,i2) ->
+                pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
+              l
+          )
 
-          (* Context management *)
-          | TacRename l ->
-            hov 1 (
-              primitive "rename" ++ brk (1,1)
-              ++ prlist_with_sep
-                (fun () -> str "," ++ brk (1,1))
-                (fun (i1,i2) ->
-                  pr.pr_name i1 ++ spc () ++ str "into" ++ spc () ++ pr.pr_name i2)
-                l
-            )
+        (* Conversion *)
+        | TacReduce (r,h) ->
+          hov 1 (
+            pr_red_expr r
+            ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+          )
+        | TacChange (op,c,h) ->
+          hov 1 (
+            primitive "change" ++ brk (1,1)
+            ++ (
+              match op with
+                  None ->
+                    mt ()
+                | Some p ->
+                  pr.pr_pattern p ++ spc ()
+                  ++ keyword "with" ++ spc ()
+            ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+          )
 
-          (* Conversion *)
-          | TacReduce (r,h) ->
-            hov 1 (
-              pr_red_expr r
-              ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
-            )
-          | TacChange (op,c,h) ->
-            hov 1 (
-              primitive "change" ++ brk (1,1)
-              ++ (
-                match op with
-                    None ->
-                      mt ()
-                  | Some p ->
-                    pr.pr_pattern p ++ spc ()
-                    ++ keyword "with" ++ spc ()
-              ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+        (* Equality and inversion *)
+        | TacRewrite (ev,l,cl,by) ->
+          hov 1 (
+            primitive (with_evars ev "rewrite") ++ spc ()
+            ++ prlist_with_sep
+              (fun () -> str ","++spc())
+              (fun (b,m,c) ->
+                pr_orient b ++ pr_multi m ++
+                  pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
+              l
+            ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
+            ++ (
+              match by with
+                | Some by -> pr_by_tactic (pr.pr_tactic ltop) by
+                | None -> mt()
             )
+          )
+        | TacInversion (DepInversion (k,c,ids),hyp) ->
+          hov 1 (
+            primitive "dependent " ++ pr_induction_kind k ++ spc ()
+            ++ pr_quantified_hypothesis hyp
+            ++ pr_with_inversion_names pr.pr_dconstr ids
+            ++ pr_with_constr pr.pr_constr c
+          )
+        | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
+          hov 1 (
+            pr_induction_kind k ++ spc ()
+            ++ pr_quantified_hypothesis hyp
+            ++ pr_with_inversion_names pr.pr_dconstr ids
+            ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
+          )
+        | TacInversion (InversionUsing (c,cl),hyp) ->
+          hov 1 (
+            primitive "inversion" ++ spc()
+            ++ pr_quantified_hypothesis hyp ++ spc ()
+            ++ keyword "using" ++ spc () ++ pr.pr_constr c
+            ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
+          )
+      )
+      in
+      pr_atom1
 
-          (* Equality and inversion *)
-          | TacRewrite (ev,l,cl,by) ->
-            hov 1 (
-              primitive (with_evars ev "rewrite") ++ spc ()
-              ++ prlist_with_sep
-                (fun () -> str ","++spc())
-                (fun (b,m,c) ->
-                  pr_orient b ++ pr_multi m ++
-                    pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
-                l
-              ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
-              ++ (
-                match by with
-                  | Some by -> pr_by_tactic (pr.pr_tactic ltop) by
-                  | None -> mt()
-              )
-            )
-          | TacInversion (DepInversion (k,c,ids),hyp) ->
-            hov 1 (
-              primitive "dependent " ++ pr_induction_kind k ++ spc ()
-              ++ pr_quantified_hypothesis hyp
-              ++ pr_with_inversion_names pr.pr_dconstr ids
-              ++ pr_with_constr pr.pr_constr c
-            )
-          | TacInversion (NonDepInversion (k,cl,ids),hyp) ->
-            hov 1 (
-              pr_induction_kind k ++ spc ()
-              ++ pr_quantified_hypothesis hyp
-              ++ pr_with_inversion_names pr.pr_dconstr ids
-              ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
-            )
-          | TacInversion (InversionUsing (c,cl),hyp) ->
-            hov 1 (
-              primitive "inversion" ++ spc()
-              ++ pr_quantified_hypothesis hyp ++ spc ()
-              ++ keyword "using" ++ spc () ++ pr.pr_constr c
-              ++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
-            )
-        )
-        in
+    let make_pr_tac pr strip_prod_binders tag_atom tag =
 
+        let extract_binders = function
+          | Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
+          | body -> ([],body) in
         let rec pr_tac inherited tac =
           let return (doc, l) = (tag tac doc, l) in
           let (strm, prec) = return (match tac with
@@ -1130,7 +1122,7 @@ module Make
             | 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_atom1 t)), ltatom
+              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
             | TacArg(_,ConstrMayEval (ConstrTerm c)) ->
@@ -1256,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;
@@ -1271,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
 
@@ -1322,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
 
@@ -1352,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)
 
@@ -1450,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