diff options
Diffstat (limited to 'plugins/ssr/ssrcommon.mli')
| -rw-r--r-- | plugins/ssr/ssrcommon.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 4b045e989..2eadd5f26 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -41,7 +41,7 @@ val nohint : 'a ssrhint (******************************** misc ************************************) -val errorstrm : Pp.std_ppcmds -> 'a +val errorstrm : Pp.t -> 'a val anomaly : string -> 'a val array_app_tl : 'a array -> 'a list -> 'a list |