diff options
| author | Pierre-Marie Pédrot | 2020-09-28 09:54:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-11 17:35:13 +0200 |
| commit | 9a026fcaeb3fa2678b9c93da8204f9f1ddcc0b31 (patch) | |
| tree | 276a153f77e1bda164ad7bbe72bef8b11285d6e2 /kernel/subtyping.ml | |
| parent | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff) | |
Remove the compare_graph field from the conversion API.
We know statically that the first thing the conversion algorithm is going to
do is to get it from the provided function, so we simply explicitly pass it
around.
Diffstat (limited to 'kernel/subtyping.ml')
0 files changed, 0 insertions, 0 deletions