diff options
| author | Arnaud Spiwack | 2015-01-06 16:09:51 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-01-06 16:10:00 +0100 |
| commit | 2b00f74f104586c8d8b205161320e850efa91268 (patch) | |
| tree | 086db10b58f0cd8e6639233ef7a4cd311d988de6 /kernel | |
| parent | 91c9e77b8d75a3c04b64337805d2ce335b27c875 (diff) | |
Fix setoid rewrite.
Because of f66b84de608830600e43f6d1a97c29226b6b58ea (Refine primitive: [unsafe] is now true by default), setoid rewrite could produce ill-typed term. Since setoid rewrite relies on the checks of refine to ensure well-typed, turned the check explicitely on with [~unsafe:false].
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions