aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pptacticsig.mli
diff options
context:
space:
mode:
Diffstat (limited to 'printing/pptacticsig.mli')
-rw-r--r--printing/pptacticsig.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index f02785a55..c08d6044d 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -50,6 +50,8 @@ module type Pp = sig
val pr_alias : (Val.t -> std_ppcmds) ->
int -> Names.KerName.t -> Val.t list -> std_ppcmds
+ val pr_alias_key : Names.KerName.t -> std_ppcmds
+
val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
val pr_raw_tactic : raw_tactic_expr -> std_ppcmds