aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/extraargs.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/extraargs.mli')
-rw-r--r--plugins/ltac/extraargs.mli10
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index acdf67779..b06f35ddc 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -14,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
@@ -55,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 :
@@ -64,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