diff options
Diffstat (limited to 'plugins/ltac/pptactic.mli')
-rw-r--r-- | plugins/ltac/pptactic.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index c14874d6c..6c09e447a 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -14,7 +14,6 @@ open Genarg open Geninterp open Names -open Misctypes open Environ open Constrexpr open Notation_gram @@ -98,7 +97,7 @@ val pr_may_eval : ('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 -> Pp.t) -> 'a and_short_name -> Pp.t +val pr_and_short_name : ('a -> Pp.t) -> 'a Stdarg.and_short_name -> Pp.t val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t val pr_evaluable_reference_env : env -> evaluable_global_reference -> Pp.t |