diff options
| author | Pierre-Marie Pédrot | 2017-03-31 22:39:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-03-31 22:39:36 +0200 |
| commit | a20494163815e4b8275c4d0412d6c857c95263f4 (patch) | |
| tree | 2771982e38f0af58cdfb2e87ade6e492a5afd314 /kernel/nativecode.ml | |
| parent | b5f07be9fdcd41fdaf73503e5214e766bf6a303b (diff) | |
Revert "Specially crafted EConstr.kind to be more efficient."
This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance
difference was not conclusive enough to pay for the code ugliness.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions