diff options
| author | Maxime Dénès | 2017-03-28 18:15:02 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-28 18:16:41 +0200 |
| commit | dc8d8daf8850ff1a414ae36c860bc925d87eab01 (patch) | |
| tree | 99fafdf4d04dcd9fe6eb15d3b561624a5344702d /kernel/nativecode.ml | |
| parent | 98e51078fa624ce780b16d8e372ef33ac97ffaee (diff) | |
Revert to incorrect heuristic in apply.
Was breaking e.g. fiat-crypto.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions