diff options
| author | Hugo Herbelin | 2018-03-28 20:18:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-03-28 20:42:48 +0200 |
| commit | 277d5c0d56e7ba79bd338e50e15bc3c6cb62fb65 (patch) | |
| tree | 125ef1fcf0faec925a51160288e80cbf4a1ba43a /dev/ci | |
| parent | e128900aee63c972d7977fd47e3fd21649b63409 (diff) | |
Getting rid of some false "collision between bound variable names" warnings.
- In a situation like "match x with ... end" with no "return" clause
we don't warn for the implicit "as x" coming from repeating "x"
- In a multiple fixpoint, we don't warn for the recursive context
being distributed several times over the different mutual
components.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions