diff options
| -rw-r--r-- | intf/tacexpr.mli | 8 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 6 | ||||
| -rw-r--r-- | printing/ppannotation.ml | 2 | ||||
| -rw-r--r-- | printing/ppannotation.mli | 1 | ||||
| -rw-r--r-- | printing/pptactic.ml | 44 | ||||
| -rw-r--r-- | printing/pptacticsig.mli | 2 | ||||
| -rw-r--r-- | printing/richprinter.ml | 1 | ||||
| -rw-r--r-- | printing/richprinter.mli | 3 |
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 |