diff options
author | 2015-01-24 09:59:27 +0100 | |
---|---|---|
committer | 2015-01-24 10:06:22 +0100 | |
commit | f4d77142a6e1d298fadf4219c46fcc9ff8abe62a (patch) | |
tree | 471d82b41044dd5a8fa9807406b89e541d386b09 /printing/miscprint.ml | |
parent | a9026275399a891d47f0d10f624a783a1afea05d (diff) |
Tentative workaround for bug #3798.
Ultimately setoid rewrite should be written in the monad to fix it properly.
Diffstat (limited to 'printing/miscprint.ml')
0 files changed, 0 insertions, 0 deletions