diff options
author | Jason Gross <jgross@mit.edu> | 2018-07-24 23:10:34 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-07-24 23:10:34 -0400 |
commit | ea1fd608e7e00d5511a1c8816a5355ab00b810af (patch) | |
tree | 89bd6c5549e8adfdd81bda0ddc8bedec66a33273 /src/Util/Notations.v | |
parent | 152094f4d9d83e4a5689536e0cd68d4f006517e1 (diff) |
Revert "Improve rewriter speed"
This reverts commit 152094f4d9d83e4a5689536e0cd68d4f006517e1.
It is actually incorrect. We need to bubble up failures, not just
let-bind the default case. Will fix tomorrow.
Diffstat (limited to 'src/Util/Notations.v')
0 files changed, 0 insertions, 0 deletions