aboutsummaryrefslogtreecommitdiff
path: root/kernel/type_errors.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-06-26 15:34:01 +0200
committerMatthieu Sozeau2014-06-26 15:44:43 +0200
commit3d351474a11ede42b8b48eda51e036eb75ecd5d9 (patch)
treeafd28f3f0b5f54f5c222eca19b3888fdaa90ee4e /kernel/type_errors.mli
parent55e46598fac67157a5b2c820be621d254581b888 (diff)
Export the right modules in Setoid, avoiding anomalies in generalized rewriting.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions