aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extraargs.ml41
-rw-r--r--plugins/ltac/extraargs.mli11
-rw-r--r--plugins/ltac/extratactics.ml41
-rw-r--r--plugins/ltac/g_auto.ml41
-rw-r--r--plugins/ltac/g_ltac.ml42
-rw-r--r--plugins/ltac/g_obligations.ml41
-rw-r--r--plugins/ltac/g_rewrite.ml41
-rw-r--r--plugins/ltac/g_tactic.ml41
-rw-r--r--plugins/ltac/pltac.ml1
-rw-r--r--plugins/ltac/pltac.mli1
-rw-r--r--plugins/ltac/pptactic.ml52
-rw-r--r--plugins/ltac/pptactic.mli81
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/ltac/rewrite.mli4
-rw-r--r--plugins/ltac/tacentries.ml1
-rw-r--r--plugins/ltac/tacentries.mli1
-rw-r--r--plugins/ltac/tacintern.ml1
-rw-r--r--plugins/ltac/tacintern.mli4
-rw-r--r--plugins/ltac/tacinterp.ml3
-rw-r--r--plugins/ltac/tacsubst.ml1
-rw-r--r--plugins/ltac/tactic_debug.mli8
-rw-r--r--plugins/ltac/tactic_option.mli2
22 files changed, 81 insertions, 100 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 72c6f90900..6097951330 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -8,7 +8,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Grammar_API
open Pp
open Genarg
open Stdarg
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 419c5e8c45..b06f35ddc4 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Tacexpr
open Names
open Constrexpr
@@ -15,13 +14,13 @@ open Misctypes
val wit_orient : bool Genarg.uniform_genarg_type
val orient : bool Pcoq.Gram.entry
-val pr_orient : bool -> Pp.std_ppcmds
+val pr_orient : bool -> Pp.t
val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
val occurrences : (int list or_var) Pcoq.Gram.entry
val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
-val pr_occurrences : int list or_var -> Pp.std_ppcmds
+val pr_occurrences : int list or_var -> Pp.t
val occurrences_of : int list -> Locus.occurrences
val wit_natural : int Genarg.uniform_genarg_type
@@ -56,7 +55,7 @@ type place = Id.t gen_place
val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
val hloc : loc_place Pcoq.Gram.entry
-val pr_hloc : loc_place -> Pp.std_ppcmds
+val pr_hloc : loc_place -> Pp.t
val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
val wit_by_arg_tac :
@@ -65,8 +64,8 @@ val wit_by_arg_tac :
Geninterp.Val.t option) Genarg.genarg_type
val pr_by_arg_tac :
- (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
- raw_tactic_expr option -> Pp.std_ppcmds
+ (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) ->
+ raw_tactic_expr option -> Pp.t
val test_lpar_id_colon : unit Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 6d80ab5494..f3f2f27e9e 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -8,7 +8,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Grammar_API
open Pp
open Genarg
open Stdarg
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 4d13d89a49..301943a509 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -8,7 +8,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Grammar_API
open Pp
open Genarg
open Stdarg
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index cc052c8a20..2ea0f60ebc 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -8,8 +8,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
-open Grammar_API
-
DECLARE PLUGIN "ltac_plugin"
open Util
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 1935d560a4..1a2d895868 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -12,7 +12,6 @@
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
-open Grammar_API
open Libnames
open Constrexpr
open Constrexpr_ops
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 3c27b27475..c874f8d5a3 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -10,7 +10,6 @@
(* Syntax for rewriting with strategies *)
-open Grammar_API
open Names
open Misctypes
open Locus
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index e539b58674..d792d4ff7d 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Pp
open CErrors
open Util
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 2adcf02e69..2c1b1067ea 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Pcoq
(* Main entry for extensions *)
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 794cb527f3..048dcc8e92 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -8,7 +8,6 @@
(** Ltac parsing entries *)
-open Grammar_API
open Loc
open Names
open Pcoq
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 327b347ec0..140cc33440 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -67,22 +67,22 @@ let declare_notation_tactic_pprule kn pt =
prnotation_tab := KNmap.add kn pt !prnotation_tab
type 'a raw_extra_genarg_printer =
- (constr_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) ->
- (tolerability -> raw_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
+ (constr_expr -> Pp.t) ->
+ (constr_expr -> Pp.t) ->
+ (tolerability -> raw_tactic_expr -> Pp.t) ->
+ 'a -> Pp.t
type 'a glob_extra_genarg_printer =
- (glob_constr_and_expr -> std_ppcmds) ->
- (glob_constr_and_expr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
+ (glob_constr_and_expr -> Pp.t) ->
+ (glob_constr_and_expr -> Pp.t) ->
+ (tolerability -> glob_tactic_expr -> Pp.t) ->
+ 'a -> Pp.t
type 'a extra_genarg_printer =
- (EConstr.constr -> std_ppcmds) ->
- (EConstr.constr -> std_ppcmds) ->
- (tolerability -> Val.t -> std_ppcmds) ->
- 'a -> std_ppcmds
+ (EConstr.constr -> Pp.t) ->
+ (EConstr.constr -> Pp.t) ->
+ (tolerability -> Val.t -> Pp.t) ->
+ 'a -> Pp.t
let keyword x = tag_keyword (str x)
let primitive x = tag_primitive (str x)
@@ -96,7 +96,7 @@ type 'a extra_genarg_printer =
| None -> assert false
| Some Refl -> x
- let rec pr_value lev v : std_ppcmds =
+ let rec pr_value lev v : Pp.t =
if has_type v Val.typ_list then
pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list)
else if has_type v Val.typ_opt then
@@ -272,7 +272,7 @@ type 'a extra_genarg_printer =
| Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg)
| _ -> None
- let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds =
+ let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t =
fun prtac symb arg -> match symb with
| Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg
| Extend.Ulist1 s | Extend.Ulist0 s ->
@@ -599,18 +599,18 @@ type 'a extra_genarg_printer =
"raw", "glob" and "typed" levels *)
type 'a printer = {
- pr_tactic : tolerability -> 'tacexpr -> std_ppcmds;
- pr_constr : 'trm -> std_ppcmds;
- pr_lconstr : 'trm -> std_ppcmds;
- pr_dconstr : 'dtrm -> std_ppcmds;
- pr_pattern : 'pat -> std_ppcmds;
- pr_lpattern : 'pat -> std_ppcmds;
- pr_constant : 'cst -> std_ppcmds;
- pr_reference : 'ref -> std_ppcmds;
- pr_name : 'nam -> std_ppcmds;
- pr_generic : 'lev generic_argument -> std_ppcmds;
- pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds;
- pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds;
+ pr_tactic : tolerability -> 'tacexpr -> Pp.t;
+ pr_constr : 'trm -> Pp.t;
+ pr_lconstr : 'trm -> Pp.t;
+ pr_dconstr : 'dtrm -> Pp.t;
+ pr_pattern : 'pat -> Pp.t;
+ pr_lpattern : 'pat -> Pp.t;
+ pr_constant : 'cst -> Pp.t;
+ pr_reference : 'ref -> Pp.t;
+ pr_name : 'nam -> Pp.t;
+ pr_generic : 'lev generic_argument -> Pp.t;
+ pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> Pp.t;
+ pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> Pp.t;
}
constraint 'a = <
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 1127c98319..0bf9bc7f62 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -9,7 +9,6 @@
(** This module implements pretty-printers for tactic_expr syntactic
objects and their subcomponents. *)
-open Pp
open Genarg
open Geninterp
open Names
@@ -24,22 +23,22 @@ type 'a grammar_tactic_prod_item_expr =
| TacNonTerm of ('a * Names.Id.t option) Loc.located
type 'a raw_extra_genarg_printer =
- (constr_expr -> std_ppcmds) ->
- (constr_expr -> std_ppcmds) ->
- (tolerability -> raw_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
+ (constr_expr -> Pp.t) ->
+ (constr_expr -> Pp.t) ->
+ (tolerability -> raw_tactic_expr -> Pp.t) ->
+ 'a -> Pp.t
type 'a glob_extra_genarg_printer =
- (glob_constr_and_expr -> std_ppcmds) ->
- (glob_constr_and_expr -> std_ppcmds) ->
- (tolerability -> glob_tactic_expr -> std_ppcmds) ->
- 'a -> std_ppcmds
+ (glob_constr_and_expr -> Pp.t) ->
+ (glob_constr_and_expr -> Pp.t) ->
+ (tolerability -> glob_tactic_expr -> Pp.t) ->
+ 'a -> Pp.t
type 'a extra_genarg_printer =
- (EConstr.t -> std_ppcmds) ->
- (EConstr.t -> std_ppcmds) ->
- (tolerability -> Val.t -> std_ppcmds) ->
- 'a -> std_ppcmds
+ (EConstr.t -> Pp.t) ->
+ (EConstr.t -> Pp.t) ->
+ (tolerability -> Val.t -> Pp.t) ->
+ 'a -> Pp.t
val declare_extra_genarg_pprule :
('a, 'b, 'c) genarg_type ->
@@ -57,61 +56,61 @@ type pp_tactic = {
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
val pr_with_occurrences :
- ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
+ ('a -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t
val pr_red_expr :
- ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
- ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
+ ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
+ ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.t
val pr_may_eval :
- ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
- ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
+ ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
+ ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
-val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
-val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t
+val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t
val pr_in_clause :
- ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+ ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
val pr_clauses : bool option ->
- ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+ ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
-val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+val pr_raw_generic : env -> rlevel generic_argument -> Pp.t
-val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+val pr_glb_generic : env -> glevel generic_argument -> Pp.t
val pr_raw_extend: env -> int ->
- ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
+ ml_tactic_entry -> raw_tactic_arg list -> Pp.t
val pr_glob_extend: env -> int ->
- ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
+ ml_tactic_entry -> glob_tactic_arg list -> Pp.t
val pr_extend :
- (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+ (Val.t -> Pp.t) -> int -> ml_tactic_entry -> Val.t list -> Pp.t
-val pr_alias_key : Names.KerName.t -> std_ppcmds
+val pr_alias_key : Names.KerName.t -> Pp.t
-val pr_alias : (Val.t -> std_ppcmds) ->
- int -> Names.KerName.t -> Val.t list -> std_ppcmds
+val pr_alias : (Val.t -> Pp.t) ->
+ int -> Names.KerName.t -> Val.t list -> Pp.t
-val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
+val pr_ltac_constant : Nametab.ltac_constant -> Pp.t
-val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
+val pr_raw_tactic : raw_tactic_expr -> Pp.t
-val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
+val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> Pp.t
-val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
+val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t
-val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> std_ppcmds
+val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> Pp.t
-val pr_hintbases : string list option -> std_ppcmds
+val pr_hintbases : string list option -> Pp.t
-val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
+val pr_auto_using : ('constr -> Pp.t) -> 'constr list -> Pp.t
-val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t
-val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
- ('b, 'a) match_rule -> std_ppcmds
+val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) ->
+ ('b, 'a) match_rule -> Pp.t
-val pr_value : tolerability -> Val.t -> std_ppcmds
+val pr_value : tolerability -> Val.t -> Pp.t
val ltop : tolerability
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index bbd7834d58..75b665aad9 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1461,7 +1461,7 @@ let solve_constraints env (evars,cstrs) =
let nf_zeta =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
-exception RewriteFailure of Pp.std_ppcmds
+exception RewriteFailure of Pp.t
type result = (evar_map * constr option * types) option option
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 35205ac58a..23767c12f5 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -61,8 +61,8 @@ val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strat
val map_strategy : ('a -> 'b) -> ('c -> 'd) ->
('a, 'c) strategy_ast -> ('b, 'd) strategy_ast
-val pr_strategy : ('a -> Pp.std_ppcmds) -> ('b -> Pp.std_ppcmds) ->
- ('a, 'b) strategy_ast -> Pp.std_ppcmds
+val pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) ->
+ ('a, 'b) strategy_ast -> Pp.t
(** Entry point for user-level "rewrite_strat" *)
val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 791b7f48db..cf676f598f 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Pp
open CErrors
open Util
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index ccd44b914e..aa8f4efe65 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -8,7 +8,6 @@
(** Ltac toplevel command entries. *)
-open Grammar_API
open Vernacexpr
open Tacexpr
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index df03c7b472..0554d43641 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Pattern
open Pp
open Genredexpr
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index ad2e709085..e3a4d5c798 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -6,8 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
-open Pp
open Names
open Tacexpr
open Genarg
@@ -56,7 +54,7 @@ val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located
val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument
(** printing *)
-val print_ltac : Libnames.qualid -> std_ppcmds
+val print_ltac : Libnames.qualid -> Pp.t
(** Reduction expressions *)
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 7b054947b7..d3e625e73a 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Constrintern
open Patternops
open Pp
@@ -2001,7 +2000,7 @@ let lift f = (); fun ist x -> Ftactic.enter begin fun gl ->
Ftactic.return (f ist env sigma x)
end
-let lifts f = (); fun ist x -> Ftactic.nf_enter begin fun gl ->
+let lifts f = (); fun ist x -> Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (sigma, v) = f ist env sigma x in
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index c1ca854334..180fb2db40 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -6,7 +6,6 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Grammar_API
open Util
open Tacexpr
open Mod_subst
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index ef6362270a..2475e41f9d 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -58,16 +58,16 @@ val db_hyp_pattern_failure :
val db_matching_failure : debug_info -> unit Proofview.NonLogical.t
(** Prints an evaluation failure message for a rule *)
-val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t
+val db_eval_failure : debug_info -> Pp.t -> unit Proofview.NonLogical.t
(** An exception handler *)
-val explain_logic_error: exn -> Pp.std_ppcmds
+val explain_logic_error: exn -> Pp.t
(** For use in the Ltac debugger: some exception that are usually
consider anomalies are acceptable because they are caught later in
the process that is being debugged. One should not require
from users that they report these anomalies. *)
-val explain_logic_error_no_anomaly : exn -> Pp.std_ppcmds
+val explain_logic_error_no_anomaly : exn -> Pp.t
(** Prints a logic failure message for a rule *)
val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
@@ -77,4 +77,4 @@ val db_breakpoint : debug_info ->
Id.t Loc.located message_token list -> unit Proofview.NonLogical.t
val extract_ltac_trace :
- ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.std_ppcmds option Loc.located
+ ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located
diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli
index dd91944d48..95cd243ec8 100644
--- a/plugins/ltac/tactic_option.mli
+++ b/plugins/ltac/tactic_option.mli
@@ -12,4 +12,4 @@ open Vernacexpr
val declare_tactic_option : ?default:Tacexpr.glob_tactic_expr -> string ->
(* put *) (locality_flag -> glob_tactic_expr -> unit) *
(* get *) (unit -> locality_flag * unit Proofview.tactic) *
- (* print *) (unit -> Pp.std_ppcmds)
+ (* print *) (unit -> Pp.t)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 18:55:32 +0000