diff options
| author | Emilio Jesus Gallego Arias | 2017-03-17 18:12:03 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-03-21 15:51:51 +0100 |
| commit | fb04bc5cae0d648c379b9eb44f8b515f8e15b854 (patch) | |
| tree | 4b4f4ee083ec31e2d635ec4a4b8b7bd5cbc38adc /kernel | |
| parent | 66a245d8055923f8807ae42ed938c1d992051749 (diff) | |
[pp] Hide the internal representation of `std_ppcmds`.
Following a suggestion by @ppedrot in #390, we require `Pp` clients to
be aware that they are using a "view" on the `std_ppcmds` type.
This is not extremely useful as people caring about the documents will
indeed have to follow changes in the view, but it costs little to play
on the safe side here for now.
We also introduce a more standard notation, `Pp.t` for the main type.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions