aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-02 22:10:15 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-03 14:00:41 +0200
commit47d4276763971f155c81f4e299d855883b6c9408 (patch)
treee367e60b40ffd74c2044d7f5e4c1dd1753ef2b3e /theories
parent04756f75bf54b1ccda8c180c62b14c5eaaaabb67 (diff)
Fixes #7641: more detailed message for disjunctive patterns with different vars.
Could still be made more detailed with more time.
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions