aboutsummaryrefslogtreecommitdiffhomepage
path: root/syntax
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-20 20:36:08 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-20 20:36:08 +0000
commit215121fb4b8676d1b8a038c66c0690388a9e8e8c (patch)
tree57b6b8e006131a9084e03c1f541b023a9f3d39c9 /syntax
parent8d478b8bacbb08d9edb6d8d1fbdea241f013b1cb (diff)
Correction des priorités des TOMATCH
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3259 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
-rw-r--r--syntax/PPCases.v10
1 files changed, 4 insertions, 6 deletions
diff --git a/syntax/PPCases.v b/syntax/PPCases.v
index 356f6b214..f8d80fd1b 100644
--- a/syntax/PPCases.v
+++ b/syntax/PPCases.v
@@ -9,10 +9,10 @@
(* $Id$ *)
Syntax constr
- level 0:
- ne_command_listcons2 [ << (NECOMMANDLIST2 $c1 ($LIST $cl)) >> ]
- -> [ $c1:L [1 0] (NECOMMANDLIST2 ($LIST $cl)) ]
- | ne_command_listone2 [ << (NECOMMANDLIST2 $c1) >> ] -> [$c1:L]
+ level 8:
+ tomatch_cons [ << (TOMATCH $c1 ($LIST $cl)) >> ]
+ -> [ $c1:L [1 0] (TOMATCH ($LIST $cl)) ]
+ | tomatch_one [ << (TOMATCH $c1) >> ] -> [$c1:L]
;
level 10:
@@ -36,8 +36,6 @@ Syntax constr
-> [ "| " $eqn [1 0] (BAREQNLIST ($LIST $leqn)) ]
| bar_eqnlist_one [ << (BAREQNLIST $eqn) >> ]
-> [ "| " $eqn ]
-
- | tomatch [ << (TOMATCH ($LIST $lc)) >> ] -> [(NECOMMANDLIST2 ($LIST $lc)):E]
;
level 10: