diff options
| author | Hugo Herbelin | 2016-03-05 18:13:23 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-03-05 20:50:24 +0100 |
| commit | c6d6e27330f0a1c9e89b6b60953d4df757edfdb8 (patch) | |
| tree | dccd305334c454e6834a019410429f51c7b6fba0 /kernel/csymtable.ml | |
| parent | 70e0d022333e0fc9e06b582f6831cbc698959cf0 (diff) | |
Exporting build_selector, a component of discriminate, for use in congruence.
Diffstat (limited to 'kernel/csymtable.ml')
0 files changed, 0 insertions, 0 deletions