aboutsummaryrefslogtreecommitdiff
path: root/dev/include
diff options
context:
space:
mode:
authorHugo Herbelin2014-12-04 10:47:31 +0100
committerHugo Herbelin2014-12-04 11:42:59 +0100
commit9fc63bfa8c8e8bc3bf835ebb2d3d444c5a6d4f9f (patch)
treece0547f9ec401d865d9f012d684967b29f80c070 /dev/include
parent84694dcd9b720d4ed7eb838ad7c5a083e7eb86fe (diff)
Reactivating option "Set Printing Existential Instances" for asking printing full instances.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions