aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-25 14:31:11 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-27 21:55:45 +0200
commit5d9cb7ad4b3e4ccc77f77456bbb9969c418fcce2 (patch)
tree2f941e85d5cef3eba857291ed5ccf47d1385ed28 /checker/univ.ml
parent0fc6d2dcdb7d12e37d43cbf44fecaf2c0fddadcc (diff)
Fixing a "This clause is redundant" error when interpreting the "in"
clause of a "match" over an irrefutable pattern.
Diffstat (limited to 'checker/univ.ml')
0 files changed, 0 insertions, 0 deletions