diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-24 17:19:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-24 17:19:26 +0000 |
| commit | ffbdf38b2d2278751ae650fbf97427f161c2e240 (patch) | |
| tree | 8c396430a61b0b24fd031cdc755328791f0c6942 /contrib | |
| parent | b42344a947a0587652b5ae3278b81996de037b6f (diff) | |
Parenthesage du terme pour accepter 'of' comme non ident
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5148 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/psyntax.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 5acfe8454..23d945c96 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; IDENT "of"; v = type_v0 -> + [ [ IDENT "array"; size = Constr.constr; IDENT "of"; v = type_v0 -> Array (size,v) | "fun"; bl = binders; c = type_c -> make_arrow bl c | c = Constr.constr -> TypePure c @@ -870,7 +870,7 @@ let pr_post_condition_opt = function let rec pr_type_v_v8 = function | Array (a,v) -> - str "array" ++ spc() ++ Ppconstrnew.pr_lconstr a ++ spc() ++ str "of " ++ + str "array" ++ spc() ++ Ppconstrnew.pr_constr a ++ spc() ++ str "of " ++ pr_type_v_v8 v | v -> pr_type_v3 v |