From c15480ebb20a791388f70f200cb08f83795007d8 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 Dec 2003 20:34:49 +0000
Subject: 'of' restait par erreur mot-cle dans psyntax.ml4 en v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5139 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/psyntax.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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	  
-- 
cgit v1.2.3