aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/pputils.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-11 21:51:23 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-07-13 15:14:45 +0200
commit9938aed874d3e15e5d21689ea841bdc3e6ebb40e (patch)
treef3c08864d8e26e29350d541904412cc07da79abf /printing/pputils.mli
parent001c95411b6674423886a085d8f624ea031a9ebc (diff)
Safer API for Global.body_of_constant and variants.
We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean.
Diffstat (limited to 'printing/pputils.mli')
0 files changed, 0 insertions, 0 deletions