From ffbdf38b2d2278751ae650fbf97427f161c2e240 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 24 Dec 2003 17:19:26 +0000 Subject: 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 --- contrib/correctness/psyntax.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'contrib/correctness/psyntax.ml4') 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 -- cgit v1.2.3