diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-17 16:52:42 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-17 16:53:15 +0200 |
commit | 77df7b1283940d979d3e14893d151bc544f41410 (patch) | |
tree | f8762ff000264c00bb9e870c5acb3ac02faea411 /kernel/reduction.mli | |
parent | 39e8010bf51b687f11d04c6a44cb959e85e86f7b (diff) |
Fix coercion code to disallow using cumulativity in the domain of products, which
results in strange changes in user provided terms.
Diffstat (limited to 'kernel/reduction.mli')
0 files changed, 0 insertions, 0 deletions