diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-30 15:43:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-07-01 16:50:17 +0200 |
| commit | dab5c4c642ee9b25d488c476d55db232cf74006b (patch) | |
| tree | 134e2cf992130de5e376306393d5e12d1528a7d1 /kernel/names.ml | |
| parent | 0917ce7cf48cadacc6fca48ba18b395740cccbe2 (diff) | |
Further simplification of the graph traversal in Univ.
We passed the arc to be marked as visited to the functions pushing the
neighbours on the remaining stack, but this can be actually done before
pushing them, as the [process_le] and [process_lt] functions do not rely
on the visited flag. This exposes more clearly the invariants of the
algorithm.
Diffstat (limited to 'kernel/names.ml')
0 files changed, 0 insertions, 0 deletions