diff options
| author | Pierre-Marie Pédrot | 2020-07-04 23:58:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-02 18:00:52 +0200 |
| commit | 7b4f197d37a5f1bdf470676f6879c607a45a3477 (patch) | |
| tree | f908ba29b9623835bad806e01e0c6ead7667727d /kernel/nativelambda.ml | |
| parent | cc51e1fd680c1f1bf47cc8b504196c9f2677fa3b (diff) | |
Use a dedicated type for equality elimination.
In this mess of higher-order callbacks it helps sorting out the invariants
of the structure.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions