diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/tacexpr.ml | 35 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 35 | ||||
| -rw-r--r-- | plugins/ltac/tactic_debug.ml | 11 |
3 files changed, 5 insertions, 76 deletions
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 11d13d3a2f..8731cbf60d 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -35,41 +35,6 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Goal_select.t = - | SelectAlreadyFocused - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectNth of int - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectList of (int * int) list - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectId of Id.t - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectAll - [@ocaml.deprecated "Use constructors in [Goal_select]"] -[@@ocaml.deprecated "Use [Goal_select.t]"] - -type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = - | ElimOnConstr of 'a - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnIdent of lident - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnAnonHyp of int - [@ocaml.deprecated "Use constructors in [Tactics]"] -[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] - -type 'a destruction_arg = - clear_flag * 'a Tactics.core_destruction_arg -[@@ocaml.deprecated "Use Tactics.destruction_arg"] - -type inversion_kind = Inv.inversion_kind = - | SimpleInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversionClear - [@ocaml.deprecated "Use constructors in [Inv]"] -[@@ocaml.deprecated "Use Tactics.inversion_kind"] - type ('c,'d,'id) inversion_strength = | NonDepInversion of Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 6b131edaac..9958d6dcda 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -35,41 +35,6 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Goal_select.t = - | SelectAlreadyFocused - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectNth of int - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectList of (int * int) list - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectId of Id.t - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectAll - [@ocaml.deprecated "Use constructors in [Goal_select]"] -[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] - -type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = - | ElimOnConstr of 'a - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnIdent of lident - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnAnonHyp of int - [@ocaml.deprecated "Use constructors in [Tactics]"] -[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] - -type 'a destruction_arg = - clear_flag * 'a Tactics.core_destruction_arg -[@@ocaml.deprecated "Use Tactics.destruction_arg"] - -type inversion_kind = Inv.inversion_kind = - | SimpleInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversionClear - [@ocaml.deprecated "Use constructors in [Inv]"] -[@@ocaml.deprecated "Use Tactics.inversion_kind"] - type ('c,'d,'id) inversion_strength = | NonDepInversion of Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 48d677a864..6bab8d0353 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -12,7 +12,6 @@ open Util open Names open Pp open Tacexpr -open Termops let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () @@ -51,8 +50,8 @@ let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) let db_pr_goal gl = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let penv = print_named_context env in - let pc = print_constr_env env (Tacmach.New.project gl) concl in + let penv = Termops.Internal.print_named_context env in + let pc = Printer.pr_econstr_env env (Tacmach.New.project gl) concl in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () @@ -243,7 +242,7 @@ let db_constr debug env sigma c = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Evaluated term: " ++ print_constr_env env sigma c) + msg_tac_debug (str "Evaluated term: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints the pattern rule *) @@ -268,7 +267,7 @@ let db_matched_hyp debug env sigma (id,_,c) ido = is_debug debug >>= fun db -> if db then msg_tac_debug (str "Hypothesis " ++ Id.print id ++ hyp_bound ido ++ - str " has been matched: " ++ print_constr_env env sigma c) + str " has been matched: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints the matched conclusion *) @@ -276,7 +275,7 @@ let db_matched_concl debug env sigma c = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env sigma c) + msg_tac_debug (str "Conclusion has been matched: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints a success message when the goal has been matched *) |