diff options
Diffstat (limited to 'src/boot/fe/ast.ml')
| -rw-r--r-- | src/boot/fe/ast.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/boot/fe/ast.ml b/src/boot/fe/ast.ml index bf7a11ff..438d9de9 100644 --- a/src/boot/fe/ast.ml +++ b/src/boot/fe/ast.ml @@ -300,7 +300,7 @@ and domain = and pat = PAT_lit of lit - | PAT_tag of ident * (pat array) + | PAT_tag of ((name identified) * (pat array)) | PAT_slot of ((slot identified) * ident) | PAT_wild |