diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-03-28 17:53:43 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-03-28 18:28:58 +0200 |
commit | d670c6b6ceab80f1c3b6b74ffb53579670c0e621 (patch) | |
tree | 38b375155df8cd81638ebcab7401d35ec8f08502 /intf/misctypes.mli | |
parent | 044d9f62bf0e1140268a3236e4bb53f10d716078 (diff) |
Fixing an incorrect use of prod_appvect on a term which was not a
product in setoid_rewrite.
Before commit e8c47b652, it was raising an error which has been turned
to an anomaly.
This impacted Compcert where the former error was (apparently) caught
so that setoid_rewrite was returning back to ordinary rewrite.
Diffstat (limited to 'intf/misctypes.mli')
0 files changed, 0 insertions, 0 deletions