diff options
| author | Matthieu Sozeau | 2018-08-15 20:14:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 11:17:56 +0100 |
| commit | 8a5cd826ee8d7d51c85c834c28f090466dda33a5 (patch) | |
| tree | 52aa7e5a2321ddac14847ef9f28e666664b4c11b /dev/base_include | |
| parent | acc4f5922dcc1f92f3dc3db653b7608949b60c2b (diff) | |
[occur_rigidly] Try improving occur-check approximation
The code is cleaner and more self-explanatory this way.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions