diff options
| author | Enrico Tassi | 2014-07-14 12:44:32 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-07-14 12:48:33 +0200 |
| commit | 8e328c6c3b2d6cfe3110abdfe5bb57eeba9c0cc4 (patch) | |
| tree | 03e9e4c6cdc662b66b7f97670af051793869e765 /kernel/nativecode.ml | |
| parent | 99cee0e8d64567c6a89ab665c6e4dfd934674142 (diff) | |
smartlocate: look for the head symbol for real
This bug was hacked around in ssreflect, but with the new idea
that parsing and interpretation are done in distinct phases the
work around could not be implemented anymore.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions