diff options
| author | filliatr | 2001-04-05 14:29:44 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-05 14:29:44 +0000 |
| commit | 763102437580da08cd96d06d05d99dc1a3eda1b1 (patch) | |
| tree | 7721eae697f75fd3769260ef8b8adc4c7b4197f7 /contrib/correctness/Arrays.v | |
| parent | def9cd8e725af360c5e528450ecd7660dcef7620 (diff) | |
mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1551 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/Arrays.v')
| -rw-r--r-- | contrib/correctness/Arrays.v | 16 |
1 files changed, 7 insertions, 9 deletions
diff --git a/contrib/correctness/Arrays.v b/contrib/correctness/Arrays.v index 6fe72671aa..794131428e 100644 --- a/contrib/correctness/Arrays.v +++ b/contrib/correctness/Arrays.v @@ -64,19 +64,17 @@ Hints Resolve new_def store_def_1 store_def_2 : datatypes v62. (* A tactic to simplify access in arrays *) -Tactic Definition ArrayAccess [$i $j $H] := - [<:tactic: < - Elim (Z_eq_dec $i $j); [ - Intro $H; Rewrite $H; Rewrite store_def_1 - | Intro $H; Rewrite store_def_2; [ Idtac | Idtac | Idtac | Exact $H ] ] - >>]. +Tactic Definition ArrayAccess i j H := + Elim (Z_eq_dec i j); [ + 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 *) -Grammar command command0 := +Grammar constr constr0 := array_access - [ ident($t) "#" "[" command($c) "]" ] -> [ <<(access $t $c)>> ]. + [ "#" ident($t) "[" constr($c) "]" ] -> [ (access $t $c) ]. Syntax constr level 0 : array_access - [ (APPLIST <<access>> ($VAR $t) $c) ] -> [ $t "#[" $c:L "]" ]. + [ << (APPLIST access ($VAR $t) $c) >> ] -> [ $t "#[" $c:L "]" ]. |