diff options
Diffstat (limited to 'plugins/ltac/pptactic.mli')
| -rw-r--r-- | plugins/ltac/pptactic.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 1f6ebaf448..d9da954fe6 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -53,6 +53,8 @@ type pp_tactic = { pptac_prods : grammar_terminals; } +val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t + val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit val pr_with_occurrences : @@ -91,7 +93,7 @@ val pr_alias_key : Names.KerName.t -> Pp.t val pr_alias : (Val.t -> Pp.t) -> int -> Names.KerName.t -> Val.t list -> Pp.t -val pr_ltac_constant : Nametab.ltac_constant -> Pp.t +val pr_ltac_constant : ltac_constant -> Pp.t val pr_raw_tactic : raw_tactic_expr -> Pp.t |