diff options
| author | Gaëtan Gilbert | 2020-05-14 11:16:23 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-14 11:16:23 +0200 |
| commit | 6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6 (patch) | |
| tree | e25e7dbdf2ba149f7ef06867448f557bb6cbcb4f /interp/notation.mli | |
| parent | 13bd7bef1f61072d62c3a0bf69148eeeac895d9f (diff) | |
| parent | f71ef93aa21cd2ed4135588db3a5a3e8b42ceb39 (diff) | |
Merge PR #12313: Make explicit that UGraph lower bounds are only of two kinds.
Reviewed-by: SkySkimmer
Diffstat (limited to 'interp/notation.mli')
0 files changed, 0 insertions, 0 deletions