diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-11 12:41:41 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-11 12:41:41 +0000 |
| commit | 4ac0580306ea9e45da1863316936d700969465ad (patch) | |
| tree | bf7595cd76895f3a349e7e75ca9d64231b01dcf8 /contrib/correctness/Arrays.v | |
| parent | 8a7452976731275212f0c464385b380e2d590f5e (diff) | |
documentation automatique de la bibliothèque standard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1578 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/Arrays.v')
| -rw-r--r-- | contrib/correctness/Arrays.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v index 794131428..10ba81719 100644 --- a/contrib/correctness/Arrays.v +++ b/contrib/correctness/Arrays.v @@ -10,9 +10,9 @@ (* $Id$ *) -(*******************************************) -(* Functional arrays, for use in Programs. *) -(*******************************************) +(**********************************************) +(* Functional arrays, for use in Correctness. *) +(**********************************************) (* This is an axiomatization of arrays. * @@ -77,4 +77,4 @@ Grammar constr constr0 := Syntax constr level 0 : array_access - [ << (APPLIST access ($VAR $t) $c) >> ] -> [ $t "#[" $c:L "]" ]. + [ << (access ($VAR $t) $c) >> ] -> [ "#" $t "[" $c:L "]" ]. |