diff options
| author | Pierre-Marie Pédrot | 2018-06-13 10:25:20 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-06-13 10:25:20 +0200 |
| commit | c1d690443589a457b18b39b7003ccb762bcf401f (patch) | |
| tree | 723f70ee85dc2b646ea19d8afa03972d21c78820 /plugins/ltac/pptactic.mli | |
| parent | 573c6d76d343cadaa68b5851fdebba937153c24d (diff) | |
| parent | 1dd682b1cafd64dd902e1ae6ea738192eb9b26db (diff) | |
Merge PR #7677: [api] Remove Misctypes
Diffstat (limited to 'plugins/ltac/pptactic.mli')
| -rw-r--r-- | plugins/ltac/pptactic.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5d2a996183..6c09e447a5 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -14,11 +14,11 @@ open Genarg open Geninterp open Names -open Misctypes open Environ open Constrexpr open Notation_gram open Tacexpr +open Tactypes type 'a grammar_tactic_prod_item_expr = | TacTerm of string @@ -97,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 |