diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-21 10:16:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-21 10:16:44 +0000 |
| commit | 8aab94b8feb99802ca558c78ab1a0a973138eb74 (patch) | |
| tree | 49d54f611d7a74ec3c3a659673bcdbcd95f40ba8 /syntax | |
| parent | f334e3e2273ea81e33cd6047d1fbdb36a0f911e4 (diff) | |
Bug qui empêchait "0" d'être parenthèsé
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3162 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'syntax')
| -rw-r--r-- | syntax/PPCases.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/syntax/PPCases.v b/syntax/PPCases.v index ff2aca9b3..3bdf47feb 100644 --- a/syntax/PPCases.v +++ b/syntax/PPCases.v @@ -40,13 +40,13 @@ Syntax constr | tomatch [ << (TOMATCH ($LIST $lc)) >> ] -> [(NECOMMANDLIST2 ($LIST $lc)):E] ; - level 10: + level 10: pattconstruct [ << (PATTCONSTRUCT $C $D ($LIST $T)) >> ] -> [(APPLIST $C $D ($LIST $T))] ; level 0: - pattconstructatomic [ << (PATTCONSTRUCT $C) >> ] -> [ $C ] + pattconstructatomic [ << (PATTCONSTRUCT $C) >> ] -> [ $C:E ] ; level 8: |