diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-02 22:10:15 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-03 14:00:41 +0200 |
| commit | 47d4276763971f155c81f4e299d855883b6c9408 (patch) | |
| tree | e367e60b40ffd74c2044d7f5e4c1dd1753ef2b3e /lib/pp.mli | |
| parent | 04756f75bf54b1ccda8c180c62b14c5eaaaabb67 (diff) | |
Fixes #7641: more detailed message for disjunctive patterns with different vars.
Could still be made more detailed with more time.
Diffstat (limited to 'lib/pp.mli')
0 files changed, 0 insertions, 0 deletions