aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppannotation.ml2
-rw-r--r--printing/ppannotation.mli1
-rw-r--r--printing/pptactic.ml44
-rw-r--r--printing/pptacticsig.mli2
-rw-r--r--printing/richprinter.ml1
-rw-r--r--printing/richprinter.mli3
6 files changed, 13 insertions, 40 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-17 22:38:22 +0000