diff options
| author | Hugo Herbelin | 2016-04-07 14:58:27 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-07 16:57:34 +0200 |
| commit | 83608720aac2a0a464649aca8b2a23ce395679ae (patch) | |
| tree | a1f72f80743b29c18a52c8281ac976d5d1cfba43 /dev/base_include | |
| parent | f6a8ce665815af9609163198f609e1db8ca49b47 (diff) | |
Fixing an incorrect use of prod_appvect on a term which was not a
product in setoid_rewrite.
Backport of d670c6b6ce from trunk.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions