From 03afe7894437cc7f3b86ece2b10107f4f928321d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 26 Nov 2002 23:37:38 +0000
Subject: Remplacement Grammar/Syntax par Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3305 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/correctness/Arrays.v | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v
index acf26ed3d5..b4367fd309 100644
--- a/contrib/correctness/Arrays.v
+++ b/contrib/correctness/Arrays.v
@@ -69,12 +69,6 @@ Tactic Definition ArrayAccess i j H :=
       Intro H; Rewrite H; Rewrite store_def_1
     | Intro H; Rewrite store_def_2; [ Idtac | Idtac | Idtac | Exact H ] ].
 
-(* Syntax and pretty-print for arrays *)
+(* Symbolic notation for access *)
 
-Grammar constr constr0 :=
-  array_access
-    [ "#" ident($t) "[" constr($c) "]" ] -> [ (access $t $c) ].
-
-Syntax constr level 0 :
-  array_access
-    [ << (access ($VAR $t) $c) >> ] -> [ "#" $t "[" $c:L "]" ].
+Notation "# t [ c ]" := (access t c) (at level 0, t ident).
-- 
cgit v1.2.3