diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-09 16:08:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-09 16:08:48 +0200 |
| commit | 834530272b9006e28a4b7ba35b1f8f861f51e7ce (patch) | |
| tree | e485fd87323492daf135d7eecbb330a9e03fc0bb /pretyping | |
| parent | f9ef634e94c667641a9da12fa2b9f8e585d6d5c6 (diff) | |
| parent | 8ad6bf357284f3fcfd94f08561450bb5bf38ad36 (diff) | |
Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while looking for a notation for a nested pattern
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions