diff options
Diffstat (limited to 'contrib/correctness/psyntax.ml4')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 402537e509..5acfe8454c 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -492,7 +492,7 @@ GEXTEND Gram | t = type_v3 -> t ] ] ; type_v3: - [ [ IDENT "array"; size = Constr.lconstr; "of"; v = type_v0 -> + [ [ IDENT "array"; size = Constr.lconstr; IDENT "of"; v = type_v0 -> Array (size,v) | "fun"; bl = binders; c = type_c -> make_arrow bl c | c = Constr.constr -> TypePure c |