diff options
Diffstat (limited to 'ide/document.mli')
| -rw-r--r-- | ide/document.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/document.mli b/ide/document.mli index fb96cb6d7..ab8e71808 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -102,7 +102,7 @@ val context : 'a document -> (id * 'a) list * (id * 'a) list (** debug print *) val print : - 'a document -> (bool -> id option -> 'a -> Pp.std_ppcmds) -> Pp.std_ppcmds + 'a document -> (bool -> id option -> 'a -> Pp.t) -> Pp.t (** Callbacks on documents *) |