diff options
| author | Emilio Jesus Gallego Arias | 2018-06-03 19:06:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-06-03 19:06:41 +0200 |
| commit | 7a59d74a8ccb62a68f0b1e460bdc39041345eba8 (patch) | |
| tree | 290d5635903a60658dfd9f19e5d00eec79027b48 /kernel/cbytecodes.ml | |
| parent | c5d6b26e8de1a32054509d11ddeeaba3b8bfd8ac (diff) | |
| parent | 47d4276763971f155c81f4e299d855883b6c9408 (diff) | |
Merge PR #7682: Fixes #7641: more detailed message about disjunctive patterns with different variables
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions