diff options
| author | Pierre-Marie Pédrot | 2020-04-02 19:11:10 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-09 13:35:52 +0200 |
| commit | 84cd299416a669c73a3357e42e589d32cb467e1d (patch) | |
| tree | 9e91cd5e8735b4a64595c443e5aa643561c65a76 /kernel/uGraph.ml | |
| parent | fce845329806096ea999f7485ffa3ab20e58b66a (diff) | |
Inline an alias-computing function only used once.
This makes some invariants explicit and is 1:1 equivalent.
Diffstat (limited to 'kernel/uGraph.ml')
0 files changed, 0 insertions, 0 deletions