diff options
| author | Hugo Herbelin | 2015-04-21 17:12:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-04-22 18:49:36 +0200 |
| commit | 3d2cf9fea0aec4ae839f70acd896958772b4caaf (patch) | |
| tree | ad3a5c758b05c19761643b9cc07ec99c3777e8cd /pretyping/patternops.ml | |
| parent | 8e5ecc6a3e334620ff6149706008fe4432567870 (diff) | |
Test for #4198 (appcontext in return clause of match).
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions